ABSTRACT. Checking the satisfiability of quantifier-free real-arithmetic formulas is a practically
highly relevant but computationally hard problem. Some beautiful mathematical decision
procedures implemented in computer algebra systems are capable of solving such problems,
however, they were developed for more general tasks like quantifier elimination, therefore
their applicability to satisfiability checking is often restricted. In computer science,
recent advances in satisfiability-modulo-theories (SMT) solving led to elegant embeddings of
such decision procedures in SMT solvers in a way that combines the strengths of symbolic
computation methods and heuristic-driven search techniques. In this talk we discuss such
embeddings and show that they might be quite challenging but can lead to powerful synergies
and open new lines of research.

ABSTRACT. Separation logic has become a stock formalism for reasoning about programs with dynamic memory allocation. We introduce a variant of separation logic that supports lists and trees as well as inductive constraints on the data stored in these structures. We prove that this logic has the small model property, meaning that for each satisfiable formula there is a small domain in which the formula is satisfiable. As a consequence, the satisfiability and entailment problems for our fragment are in NP and coNP, respectively. Leveraging this result, we describe a polynomial SMT encoding that allows us to decide satisfiability and entailment for our separation logic.

ABSTRACT. We study probabilistic reasoning in a context that allows for "partial truths", investigating computational and algorithmic properties of non-classical Lukasiewicz Infinitely-valued Probabilistic Logic. In particular, we study the decision problem over Lukasiewicz Infinitely-valued Probabilistic assignments which we call LIPSAT. Although the search space is initially infinite, we provide linear algebraic methods that guarantee polynomial size witnesses, so that the problem is shown to be NP-complete. An exact algorithm is presented which employs, as a subroutine, the decision problem for Lukasiewicz Infinitely-valued (Non-Probabilistic) Logic, which is also an NP-complete problem. We develop implementations of the algorithms described and discuss the empirical presence of a phase transition behavior for those problems.

ABSTRACT. Codd's rule of entity integrity stipulates that every table in a database must have a primary key. This means that the attributes that form the primary key must carry no missing information and have unique value combinations. In practice, and in particular in modern applications, data records cannot always meet such requirements. Previous work has proposed the notion of a key set, which can identify more data records uniquely when information is missing. Apart from the proposal, key sets have not been investigated much further in the literature or in real systems. We outline important database applications, and investigate computational limits and techniques to reason automatically about key sets. We establish a binary axiomatization for the implication problem of key sets, and prove its coNP-completeness. In addition, we show that perfect models do not always exist for key sets. Finally, we show that the implication problem for unary key sets by arbitrary key sets has better computational properties. The fragment enjoys a unary axiomatization, is decidable in time quadratic in the input, and perfect models can always be generated.

ABSTRACT. In this paper we present an abstraction-refinement framework for reasoning with large theories. We consider several types of abstractions based on over and under approximations of first-order theories. We implemented the proposed approached in a theorem prover iProver and evaluated over the TPTP library.

ABSTRACT. The automated theorem prover Leo-III for classical higher-order logic with Henkin semantics and choice is presented. Leo-III is based on extensional higher-order paramodulation and accepts every common TPTP dialect (FOF, TFF, THF), including their recent extensions to rank-1 polymorphism (TF1, TH1). In addition, the prover natively supports almost every normal higher-order modal logic. Leo-III cooperates with first-order reasoning tools using translations to (polymorphic) many-sorted first-order logic and produces verifiable proof certificates. The prover is evaluated on heterogeneous benchmark sets.

ABSTRACT. ATPboost is a system for solving sets of large-theory problems by interleaving ATP runs with state-of-the-art machine learning of premise selection from the proofs. Unlike many previous approaches that use multilabel setting, the learning is implemented as binary classification that estimates the pairwise-relevance of ( theorem, premise ) pairs. ATPboost uses for this the XGBoost gradient boosting algorithm, which is fast and has state-of-the-art performance on many tasks. Learning in the binary setting however requires negative examples, which is nontrivial due to many alternative proofs. We discuss and implement several solutions in the context of the ATP/ML feedback loop, and show that ATPboost with such methods significantly outperforms the k-nearest neighbors multilabel classifier.

ABSTRACT. We present Cubicle-W, a new version of the Cubicle model checker to verify parameterized systems under weak memory models. Its main originality is to implement a backward reachability algorithm modulo weak memory reasoning using SMT. Our experiments show that Cubicle-W is expressive and efficient enough to automatically prove safety of concurrent algorithms, for an arbitrary number of processes, ranging from mutual exclusion to synchronization barriers.

ABSTRACT. The equational reasoning tool MaedMax implements maximal ordered completion. This new approach extends the maxSMT-based method for standard completion developed by Klein and Hirokawa (2011) to ordered completion and theorem proving. MaedMax incorporates powerful ground completeness checks and supports certification of proofs by an Isabelle-based certifier. It also provides an order generation mode which can be used to synthesize term orderings for other tools. Experiments show the potential of our approach.

ABSTRACT. In this paper we describe the infrastructure supporting confluence tools and competitions: Cops, the confluence problems database, and CoCoWeb, a convenient web interface for tools that participate in the annual confluence competition.

ABSTRACT. FORT is a tool that implements the first-order theory of rewriting for the decidable class of left-linear right-ground rewrite systems. It can be used to decide properties of a given rewrite system and to synthesize rewrite systems that satisfy arbitrary properties expressible in the first-order theory of rewriting. In this paper we report on the extensions that were incorporated in the latest release (2.0) of FORT. These include witness generation for existentially quantified variables in formulas, support for combinations of rewrite systems, as well as an extension to deal with non-ground terms for properties related to confluence.