Automated Reasoning

Several applications from program analysis, design and testing rely critically on solving SMT problems. Many applications build on top of SMT solvers in sophisticated ways by carefully crafting the solver interaction.We illustrate partial correctness checking as an SMT problem and we introduce a procedure for model finding of recursive Horn clauses with arithmetic.

In mathematics sometimes methods from one area can be fruitfully applied for getting results in another area, occasionally looking very remote from the other area. A well-known example is given by analytic geometry that enables us, besides proving “elementary” geometrical theorems, to establish otherwise untractable results like unsolvability of the problems of angle trisection and doubling the cube by compass and straightedge and to reduce calculation of the kissing numbers of spheres to verification of a first-order formula about real numbers (and that could be done, in principle, by Tarski algorithm).

The aim of this invited talk is to discuss strengths, limitations and challenges around one of the simplest yet most powerful practical automated deduction formalisms, namely propositional SAT and its extensions. We will see some of the reasons why

CDCL SAT solvers

are so effective for finding solutions to so diverse real-world problems, using a single fully automatic push-button strategy, and, by extending them to SAT Modulo Theories (SMT), also to optimization problems and problems with complex (e.g., arithmetic) constraints for which a full encoding into SAT would be too large and/or inefficient. We will give some examples of trade-offs regarding full SAT encodings vs SMT theory solvers, and discuss why SAT and even SMT are just binary resolution strategies, the consequences of this fact, and possible ways to overcome it. Many aspects of the discussion carry over to first-order logic and beyond.

Unification modulo the theory defined by a single equation which specifies that a binary operator distributes synchronously over another binary operator is shown to be undecidable. It is the simplest known theory, to our knowledge, for which unification is undecidable: it has only one defining axiom and moreover, every congruence class is finite (so the matching problem is decidable).

Unification in Description Logics has been proposed as an inference service that can, for example, be used to detect redundancies in ontologies. For the Description Logic

$\mathcal{EL}$

, which is used to define several large biomedical ontologies, unification is

NP

-complete. An NP unification algorithm for

$\mathcal{EL}$

based on a translation into propositional satisfiability (SAT) has recently been presented. In this paper, we extend this SAT encoding in two directions: on the one hand, we add general concept inclusion axioms, and on the other hand, we add role hierarchies (

$\mathcal{H}$

) and transitive roles (

R

 + 

). For the translation to be complete, however, the ontology needs to satisfy a certain cycle restriction. The SAT translation depends on a new rewriting-based characterization of subsumption w.r.t.

$\mathcal{ELH}_{{R}^+}$

-ontologies.

UEL is a system that computes unifiers for unification problems formulated in the description logic

$\mathcal{EL}$

.

$\mathcal{EL}$

is a description logic with restricted expressivity, but which is still expressive enough for the formal representation of biomedical ontologies, such as the large medical ontology SNOMED CT. We propose to use UEL as a tool to detect redundancies in such ontologies by computing unifiers of two formal concepts suspected of expressing the same concept of the application domain. UEL can be used as a plug-in of the popular ontology editor Protégé, or as a standalone unification application.

We provide a systematic and modular method to define non-deterministic finite-valued semantics for a natural and very general family of

canonical labelled calculi

, of which many previously studied sequent and labelled calculi are particular instances. This semantics is

effective

, in the sense that it naturally leads to a decision procedure for these calculi. It is then applied to provide simple

decidable

semantic criteria for crucial syntactic properties of these calculi, namely (strong) analyticity and cut-admissibility.

This paper describes a novel decision procedure for quantifier-free linear integer arithmetic. Standard techniques usually relax the initial problem to the rational domain and then proceed either by projection (

e.g.

Omega-Test

) or by branching/cutting methods (

branch-and-bound

,

branch-and-cut

,

Gomory cuts

). Our approach tries to bridge the gap between the two techniques: it interleaves an exhaustive search for a model with bounds inference. These bounds are computed provided an oracle capable of finding constant positive linear combinations of affine forms. We also show how to design an efficient oracle based on the Simplex procedure. Our algorithm is proved sound, complete, and terminating and is implemented in the

alt-ergo

theorem prover. Experimental results are promising and show that our approach is competitive with state-of-the-art SMT solvers.

Fuzzy Description Logics (DLs) with t-norm semantics have been studied as a means for representing and reasoning with vague knowledge. Recent work has shown that even fairly inexpressive fuzzy DLs become undecidable for a wide variety of t-norms. We complement those results by providing a class of t-norms and an expressive fuzzy DL for which ontology consistency is linearly reducible to crisp reasoning, and thus has its same complexity. Surprisingly, in these same logics crisp models are insufficient for deciding fuzzy subsumption.

In intuitionistic sequent calculi, detecting that a sequent is unprovable is often used to direct proof search. This is for instance seen in backward chaining, where an unprovable subgoal means that the proof search must backtrack. In undecidable logics, however, proof search may continue indefinitely, finding neither a proof nor a disproof of a given subgoal.

In this paper we characterize a family of truth-preserving abstractions from intuitionistic first-order logic to the monadic fragment of classical first-order logic. Because they are truthful, these abstractions can be used to disprove sequents in intuitionistic first-order logic.

Satallax is an automatic higher-order theorem prover that generates propositional clauses encoding (ground) tableau rules and uses MiniSat to test for unsatisfiability. We describe the implementation, focusing on flags that control search and examples that illustrate how the search proceeds.

The use of interpolants in verification is gaining more and more importance. Since theories used in applications are usually obtained as (disjoint) combinations of simpler theories, it is important to modularly re-use interpolation algorithms for the component theories. We show that a sufficient and necessary condition to do this for quantifier-free interpolation is that the component theories have the ‘strong (sub-)amalgamation’ property. Then, we provide an equivalent syntactic characterization, identify a sufficient condition, and design a combined quantifier-free interpolation algorithm handling both convex and non-convex theories, that subsumes and extends most existing work on combined interpolation.

The problem of SPARQL query containment is defined as determining if the result of one query is included in the result of another for any RDF graph. Query containment is important in many areas, including information integration, query optimization, and reasoning about Entity-Relationship diagrams. We encode this problem into an expressive logic called

μ

-calculus: where RDF graphs become transition systems, queries and schema axioms become formulas. Thus, the containment problem is reduced to formula satisfiability test. Beyond the logic’s expressive power, satisfiability solvers are available for it. Hence, this study allows to exploit these advantages.

We present a fully automated method for the verification of annotated recursive programs with dynamic pointer structures. Assertions are expressed in a dialect of dynamic logic extended with nominals and tailored to heap structures, in which one can express complex reachability properties. Verification conditions are generated using a novel calculus for computing the strongest postcondition of statements manipulating the heap, such as dynamic allocation and field-assignment. Further, we introduce a new decidable tableaux-based method and its prototype implementation to automatically check these verification conditions.

When formally analyzing security protocols it is often important to express properties in terms of an adversary’s inability to distinguish two protocols. It has been shown that this problem amounts to deciding the equivalence of two constraint systems,

i.e.

, whether they have the same set of solutions. In this paper we study this equivalence problem when cryptographic primitives are modeled using a group equational theory, a special case of monoidal equational theories. The results strongly rely on the isomorphism between group theories and rings. This allows us to reduce the problem under study to the problem of solving systems of equations over rings. We provide several new decidability and complexity results, notably for equational theories which have applications in security protocols, such as exclusive or and Abelian groups which may additionally admit a unary, homomorphic symbol.

Reachability and LTL model-checking problems for flat counter systems are known to be decidable but whereas the reachability problem can be shown in NP, the best known complexity upper bound for the latter problem is made of a tower of several exponentials. Herein, we show that the problem is only NP-complete even if LTL admits pasttime operators and arithmetical constraints on counters. Actually, the NP upper bound is shown by adequately combining a new stuttering theorem for Past LTL and the property of small integer solutions for quantifier-free Presburger formulae. Other complexity results are proved, for instance for restricted classes of flat counter systems.

We present a modification of the superposition calculus that is meant to generate explanations why a set of clauses is satisfiable. This process is related to abductive reasoning, and the explanations generated are clauses constructed over so-called abductive constants. We prove the correctness and completeness of the calculus in the presence of redundancy elimination rules, and develop a sufficient condition guaranteeing its termination; this sufficient condition is then used to prove that all possible explanations can be generated in finite time for several classes of clause sets, including many of interest to the SMT community. We propose a procedure that generates a set of explanations that should be useful to a human user and conclude by suggesting several extensions to this novel approach.

We propose a word level, bounded model checking (BMC) algorithm based on translation into the effectively propositional fragment (EPR) of first-order logic. This approach to BMC allows for succinct representation of unrolled transition systems and facilitates reasoning at a higher level of abstraction. We show that the proposed approach can be scaled to industrial hardware model checking problems involving memories and bit-vectors. Another contribution of this work is in generating challenging benchmarks for first-order theorem provers based on the proposed encoding of real-life hardware verification problems into EPR. We report experimental results for these problems for several provers known to be strong in EPR problem solving. A number of these benchmarks have already been released to the TPTP library.

We introduce a technique to prove non-termination of term rewrite systems automatically. Our technique improves over previous approaches substantially, as it can also detect non-looping non-termination.

This paper presents new results on the decidability of inductive validity of conjectures. For these results, a class of term rewrite systems (TRSs) with built-in linear integer arithmetic is introduced and it is shown how these TRSs can be used in the context of inductive theorem proving. The proof method developed for inductive theorem proving couples (implicit) inductive reasoning with a decision procedure for the theory of linear integer arithmetic with (free) constructors. The effectiveness of the new decidability results on a large class of conjectures is demonstrated by an evaluation of the prototype implementation

Sail2

.

Combination of theories underlies the design of satisfiability modulo theories (SMT) solvers. The Nelson-Oppen framework can be used to build a decision procedure for the combination of two disjoint decidable stably infinite theories.

We here study combinations involving an arbitrary first-order theory. Decidability is lost, but refutational completeness is preserved. We consider two cases and provide complete (semi-)algorithms for them. First, we show that it is possible under minor technical conditions to combine a decidable (not necessarily stably infinite) theory and a disjoint finitely axiomatized theory, obtaining a refutationally complete procedure. Second, we provide a refutationally complete procedure for the union of two disjoint finitely axiomatized theories, that uses the assumed procedures for the underlying theories without modifying them.

Regular algebras axiomatise the equational theory of regular expressions. We use Isabelle/HOL’s automated theorem provers and counterexample generators to study the regular algebras of Boffa, Conway, Kozen and Salomaa, formalise their soundness and completeness (relative to a deep result by Krob) and engineer their hierarchy. Proofs range from fully automatic axiomatic and inductive calculations to integrated higher-order reasoning with numbers, sets and monoid submorphisms. In combination with Isabelle’s simplifiers and structuring mechanisms, automated deduction provides powerful support to the working mathematician beyond first-order reasoning.

We introduce the notion of “

δ

-complete decision procedures” for solving SMT problems over the real numbers, with the aim of handling a wide range of nonlinear functions including transcendental functions and solutions of Lipschitz-continuous ODEs. Given an SMT problem

ϕ

and a positive rational number

δ

, a

δ

-complete decision procedure determines either that

ϕ

is unsatisfiable, or that the “

δ

-weakening” of

ϕ

is satisfiable. Here, the

δ

-weakening of

ϕ

is a variant of

ϕ

that allows

δ

-bounded numerical perturbations on

ϕ

. We establish the existence and complexity of

δ

-complete decision procedures for bounded SMT over reals with functions mentioned above. We propose to use

δ

-completeness as an ideal requirement for numerically-driven decision procedures. As a concrete example, we formally analyze the DPLL〈ICP〉 framework, which integrates Interval Constraint Propagation in DPLL(T), and establish necessary and sufficient conditions for its

δ

-completeness. We discuss practical applications of

δ

-complete decision procedures for correctness-critical applications including formal verification and theorem proving.

We give Binary Decision Diagram (BDD) based methods for deciding validity and satisfiability of propositional Intuitionistic Logic

Int

and Bi-intuitionistic Tense Logic

BiKt

. We handle intuitionistic implication and bi-intuitionistic exclusion by treating them as modalities, but the move to an intuitionistic basis requires careful analysis for handling the reflexivity, transitivity and antisymmetry of the underlying Kripke relation.

BiKt

requires a further extension to handle the interactions between the intuitionistic and modal binary relations, and their converses. We explain our methodology for using the Kripke semantics of these logics to constrain the underlying least and greatest fixpoint approaches of the finite model construction. With some optimisations this technique is competitive with the state of the art theorem provers for Intuitionistic Logic using the ILTP benchmark and randomly generated formulae.

In the regular model-checking framework, reachability analysis can be guided by temporal logic properties, for instance to achieve the counter example guided abstraction refinement (CEGAR) objectives. A way to perform this analysis is to translate a temporal logic formula expressed on maximal rewriting words into a “rewrite proposition” – a propositional formula whose atoms are language comparisons, and then to generate semi-decision procedures based on (approximations of) the rewrite proposition. This approach has recently been studied using a nonautomatic translation method. The extent to which such a translation can be systematised needs to be investigated, as well as the applicability of approximated methods wherever no exact translation can be effected. This paper presents contributions to that effect: (1) we investigate suitable semantics for LTL on maximal rewriting words and their influence on the feasibility of a translation, and (2) we propose a general scheme providing exact results on a fragment of LTL corresponding mainly to safety formulæ, and approximations on a larger fragment.

We propose a method which allows us to develop tableaux modulo theories using the principles of superdeduction, among which the theory is used to enrich the deduction system with new deduction rules. This method is presented in the framework of the

Zenon

automated theorem prover, and is applied to the set theory of the

B

method. This allows us to provide another prover to

Atelier B

, which can be used to verify

B

proof rules in particular. We also propose some benchmarks, in which this prover is able to automatically verify a part of the rules coming from the database maintained by

Siemens IC-MOL.

We present a new algorithm for deciding satisfiability of non-linear arithmetic constraints. The algorithm performs a Conflict-Driven Clause Learning (CDCL)-style search for a feasible assignment, while using projection operators adapted from cylindrical algebraic decomposition to guide the search away from the conflicting states.

Decision procedures for Boolean satisfiability (SAT), especially modern conflict-driven clause learning (CDCL) solvers, act routinely as core solving engines in various real-world applications. Preprocessing, i.e., applying formula rewriting/simplification rules to the input formula before the actual search for satisfiability, has become an essential part of the SAT solving tool chain. Further, some of the strongest SAT solvers today add more reasoning to search by

interleaving

formula simplification and CDCL search. Such

inprocessing SAT solvers

witness the fact that implementing additional deduction rules in CDCL solvers leverages the efficiency of state-of-the-art SAT solving further. In this paper we establish formal underpinnings of inprocessing SAT solving via an abstract inprocessing framework that covers a wide range of modern SAT solving techniques.

We present a new version of the

CEX

versioning tool for ontologies.

CEX

detects logical differences between acyclic terminologies in the lightweight description logic

$\mathcal{EL}$

with role inclusions and domain and range restrictions. Depending on the application,

CEX

outputs differences between terminologies that capture derived concept inclusions, answers to instance queries, and answers to conjunctive queries. Experiments with versions of the NCI ontology are conducted to evaluate the performance of

CEX

and compare the three types of differences.

In this paper, an overview of state-of-the-art techniques for premise selection in large theory mathematics is provided, and new premise selection techniques are introduced. Several evaluation metrics are introduced, compared and their appropriateness is discussed in the context of automated reasoning in large theory mathematics. The methods are evaluated on the MPTP2078 benchmark, a subset of the Mizar library, and a 10% improvement is obtained over the best method so far.

The full branching time logic

ctl*

is a well-known specification logic for reactive systems. Its satisfiability and model checking problems are well understood. However, it is still lacking a satisfactory sound and complete axiomatisation. The only proof system known for

ctl*

is Reynolds’ which comes with an intricate and long completeness proof and, most of all, uses rules that do not possess the subformula property.

In this paper we consider a large fragment of

ctl*

which is characterised by disallowing certain nestings of temporal operators inside universal path quantifiers. This subsumes

ctl

 + 

for instance. We present infinite satisfiability games for this fragment. Winning strategies for one of the players represent infinite tree models for satisfiable formulas. These can be pruned into finite trees using fixpoint strengthening and some simple combinatorial machinery such that the results represent proofs in a Hilbert-style axiom system for this fragment. Completeness of this axiomatisation is a simple consequence of soundness of the satisfiability games.

An algorithm for unification modulo

one-sided

distributivity is an early result by Tiden and Arnborg [14]. Unfortunately the algorithm presented in the paper, although correct, has recently been shown not to be polynomial time bounded as claimed [11]. In addition, for some instances, there exist most general unifiers that are exponentially large with respect to the input size. In this paper we first present a new polynomial time algorithm that solves the

decision

problem for a non-trivial subcase, based on a typed theory, of unification modulo one-sided distributivity. Next we present a new polynomial algorithm that solves the

decision

problem for unification modulo one-sided distributivity. A construction, employing string compression, is used to achieve the polynomial bound.

A variable

v

reaches a variable

w

if there is a path from the memory location bound to

v

to the one bound to

w

. This information is important for improving the precision of other static analyses, such as side-effects, field initialization, cyclicity and path-length, as well as of more complex analyses built upon them, such as nullness and termination. We present a provably correct constraint-based reachability analysis for Java bytecode. Our constraint is a graph whose nodes are program points and whose arcs propagate reachability information according to the semantics of bytecodes. The analysis has been implemented in the Julia static analyzer. Experiments that we performed on non-trivial Java and Android programs show a gain in precision due to a reachability information, whose presence also reduces the cost of nullness and termination analyses.

We propose a new logic, called

differential dynamic game logic

(

${\sf dDG}{\mathcal{L}}$

), that adds several game constructs on top of differential dynamic logic (

${\sf d}\mathcal{L}$

) so that it can be used for hybrid games. The logic

${\sf dDG}{\mathcal{L}}$

is a conservative extension of

${\sf d}\mathcal{L}$

, which we exploit for our implementation of

${\sf dDG}{\mathcal{L}}$

in the theorem prover KeYmaera. We provide rules for extending the

${\sf d}\mathcal{L}$

sequent proof calculus to handle the

${\sf dDG}{\mathcal{L}}$

constructs by identifying analogs to operators of

${\sf d}\mathcal{L}$

. We have implemented

${\sf dDG}{\mathcal{L}}$

in an extension of KeYmaera and verified a case study in which a robot satisfies a joint safety and liveness objective in a factory automation scenario, in which the factory may perform interfering actions independently.

The Quantified Modal Logic Theorem Proving (QMLTP) library provides a platform for testing and evaluating automated theorem proving (ATP) systems for first-order modal logics. The main purpose of the library is to stimulate the development of new modal ATP systems and to put their comparison onto a firm basis. Version 1.1 of the QMLTP library includes 600 problems represented in a standardized extended TPTP syntax. Status and difficulty rating for all problems were determined by running comprehensive tests with existing modal ATP systems. In the presented version 1.1 of the library the modal logics K, D, T, S4 and S5 with constant, cumulative and varying domains are considered. Furthermore, a small number of problems for multi-modal logic are included as well.

The diagram-based method to prove correctness of program transformations includes the computation of (critical) overlappings between the analyzed program transformation and the (standard) reduction rules which result in so-called forking diagrams. Such diagrams can be seen as rewrite rules on reduction sequences which abstract away the expressions and allow additional expressive power, like transitive closures of reductions. In this paper we clarify the meaning of forking diagrams using interpretations as infinite term rewriting systems. We then show that the termination problem of forking diagrams as rewrite rules can be encoded into the termination problem for conditional integer term rewriting systems, which can be solved by automated termination provers. Since the forking diagrams can be computed automatically, the results of this paper are a big step towards a fully automatic prover for the correctness of program transformations.

Indexing is critical for the performance of first-order theorem provers. We introduce

fingerprint indexing

, a non-perfect indexing technique that is based on short, constant length vectors of samples of term positions (“fingerprints”) organized in a trie. Fingerprint indexing supports matching and unification as retrieval relations. The algorithms are simple, the indices are small, and performance is very good in practice.

We demonstrate the performance of the index both in relative and absolute terms using large-scale profiling.

In the contexts of automated reasoning and formal verification, important

decision

problems are effectively encoded into Satisfiability Modulo Theories (SMT). In the last decade efficient SMT solvers have been developed for several theories of practical interest (e.g., linear arithmetic, arrays, bit-vectors). Surprisingly, very little work has been done to extend SMT to deal with

optimization

problems; in particular, we are not aware of any work on SMT solvers able to produce solutions which minimize cost functions over

arithmetical

variables. This is unfortunate, since some problems of interest require this functionality.

In this paper we start filling this gap. We present and discuss two general procedures for leveraging SMT to handle the minimization of

${\mathcal LA}$

(ℚ) cost functions, combining SMT with standard minimization techniques. We have implemented the procedures within the MathSAT SMT solver. Due to the absence of competitors in AR and SMT domains, we have experimentally evaluated our implementation against state-of-the-art tools for the domain of

linear generalized disjunctive programming (LGDP)

, which is closest in spirit to our domain, on sets of problems which have been previously proposed as benchmarks for the latter tools. The results show that our tool is very competitive with, and often outperforms, these tools on these problems, clearly demonstrating the potential of the approach.

We propose to describe computations using QFPAbit, a language of quantifier-free linear arithmetic on unbounded integers with bitvector operations. We describe an algorithm that, given a QFPAbit formula with input and output variables denoting integers, generates an efficient function from a sequence of inputs to a sequence of outputs, whenever such function on integers exists. The starting point for our method is a polynomial-time translation mapping a QFPAbit formula into the sequential circuit that checks the correctness of the input/output relation. From such a circuit, our synthesis algorithm produces solved circuits from inputs to outputs that are no more than singly exponential in size of the original formula. In addition to the general synthesis algorithm, we present techniques that ensure that, for example, multiplication and division with large constants do not lead to an exponential blowup, addressing a practical problem with a previous approach that used the MONA tool to generate the specification automata.

With this contribution we push the boundary of some known optimisations such as caching to the very expressive Description Logic

$\mathcal{SROIQ}$

. The developed method is based on a sophisticated dependency management and a precise unsatisfiability caching technique, which further enables better informed tableau backtracking and more efficient pruning. Additionally, we optimise the handling of cardinality restrictions, by introducing a strategy called pool-based merging.

We empirically evaluate the proposed optimisations within the novel reasoning system Konclude and show that the proposed optimisations indeed result in significant performance improvements.

This paper describes a tool for Knuth-Bendix completion. In its interactive mode the user only has to select the orientation of equations into rewrite rules; all other computations (including necessary termination checks) are performed internally. Apart from the interactive mode, the tool also provides a fully automatic mode. Moreover, the generation of (dis)proofs in equational logic is supported. Finally, the tool outputs proofs in a certifiable format.

Labelled superposition (LPSup) is a new calculus for PLTL. One of its distinguishing features, in comparison to other resolution-based approaches, is its ability to construct partial models on the fly. We use this observation to design a new decision procedure for the logic, where the models are effectively used to guide the search. On a representative set of benchmarks, our implementation is then shown to considerably advance the state of the art.

Proof systems for logics with recursive definitions typically impose a strict syntactic stratification on the body of a definition to ensure cut elimination and consistency of the logics, i.e., by forbidding any negative occurrences of the predicate being defined. Often such a restriction is too strong, as there are cases where such negative occurrences do not lead to inconsistency. Several logical frameworks based on logics of definitions have been used to mechanise reasoning about properties of operational semantics and type systems. However, some of the uses of these frameworks actually go beyond what is justified by their logical foundations, as they admit definitions which are not strictly stratified, e.g., in the formalisation of logical-relation type of arguments in typed

λ

-calculi. We consider here a more general notion of stratification, which allows one to admit some definitions that are not strictly stratified. We outline a novel technique to prove consistency and a partial cut elimination result, showing that every derivation can be transformed into a certain head normal form, by simulating its cut reductions in an infinitary proof system. We demonstrate this technique for a specific logic, but it can be extended to other richer logics.

We present Diabelli, a formal reasoning system that enables users to construct so-called heterogeneous proofs that intermix sentential formulae with diagrams.