Automated Deduction - CADE-25

On the fiftieth anniversary of the appearance of Robinson’s resolution paper [

57

], it is appropriate to consider the history and status of theorem proving, as well as its possible future directions. Here we discuss the history of first-order theorem proving both before and after 1965, with some personal reflections. We then generalize model-based reasoning to first-order provers, and discuss what it means for a prover to be goal sensitive. We also present a way to analyze asymptotically the size of the search space of a first-order prover in terms of the size of a minimal unsatisfiable set of ground instances of a set of first-order clauses.

The growing use of the internet for collaboration, and of numeric and symbolic software to perform calculations it is impossible to do by hand, not only augment the capabilities of mathematicians, but also afford new ways of observing what they do. In this essay we look at four case studies to see what we can learn about the everyday practice of mathematics: the

polymath

experiments for the collaborative production of mathematics, which tell us about mathematicians attitudes to working together in public; the

minipolymath

experiments in the same vein, from which we can examine in finer grained detail the kinds of activities that go on in developing a proof; the mathematical questions and answers in

math overflow

, which tell us about mathematical-research-in-the-small; and finally the role of computer algebra, in particular the GAP system, in the production of mathematics. We conclude with perspectives on the role of computational logic.

This paper discusses the use of first order automated reasoning in question answering and cognitive computing. For this the natural language question answering project LogAnswer is briefly depicted and the challenges faced therein are addressed. This includes a treatment of query relaxation, web-services, large knowledge bases and co-operative answering. In a second part a bridge to human reasoning as it is investigated in cognitive psychology is constructed by using standard deontic logic.

Our computational metaphysics group describes its use of automated reasoning tools to study Leibniz’s theory of concepts. We start with a reconstruction of Leibniz’s theory within the theory of abstract objects (henceforth ‘object theory’). Leibniz’s theory of concepts, under this reconstruction, has a non-modal algebra of concepts, a concept-containment theory of truth, and a modal metaphysics of complete individual concepts. We show how the object-theoretic reconstruction of these components of Leibniz’s theory can be represented for investigation by means of automated theorem provers and finite model builders. The fundamental theorem of Leibniz’s theory is derived using these tools.

Confluence is one of the central properties of rewriting. Our competition aims to foster the development of techniques for proving/disproving confluence of various formalisms of rewriting automatically. We explain the background and setup of the 4th Confluence Competition.

The termination competition focuses on automated termination analysis for all kinds of programming paradigms, including categories for term rewriting, imperative programming, logic programming, and functional programming. Moreover, the competition also features categories for automated complexity analysis. In all categories, the competition also welcomes the participation of tools providing certified proofs. The goal of the termination competition is to demonstrate the power of the leading tools in each of these areas.

A term is

weakly shallow

if each defined function symbol occurs either at the root or in the ground subterms, and a term rewriting system is weakly shallow if both sides of a rewrite rule are weakly shallow. This paper proves that non-

E

-overlapping, weakly-shallow, and non-collapsing term rewriting systems are confluent by extending

reduction graph

techniques in our previous work [

19

] with

towers of expansions

.

We present a confluence tool for left-linear term rewrite systems. The tool proves confluence by using Hindley’s commutation theorem together with three commutation criteria, including Church-Rosser modulo associative and/or commutative theories. Despite a small number of its techniques, experiments show that the tool is comparable to recent powerful confluence tools.

We consider an extension of term rewriting rules with context constraints restricting the application of rewriting to positions whose prefix (

i.e.

the sequence of symbols from the rewrite position up to the root) belongs to a given regular language. This approach, well studied in string rewriting, is similar to node selection mechanisms in XML transformation languages, and also generalizes the context-sensitive rewriting. The systems defined this way are called prefix constrained TRS (

p

CTRS), and we study the decidability of reachability of regular tree model checking and the preservation of regularity for some subclasses. The two latter properties hold for linear and right-shallow standard TRS but not anymore when adding context constraints. We show that these properties can be restored by restricting derivations to bottom-up ones, and moreover that it implies that left-linear and right-ground

p

CTRS preserve regularity and have a decidable regular model checking problem.

This paper describes two advancements of SAT-based Knuth-Bendix completion as implemented in

Maxcomp

. (1) Termination techniques using the dependency pair framework are encoded as satisfiability problems, including dependency graph and reduction pair processors. (2) Instead of relying on pure maximal completion, different SAT-encoded control strategies are exploited.

Experiments show that these developments let

Maxcomp

improve over other automatic completion tools, and produce novel complete systems.

Relative termination, a generalized notion of termination, has been used in a number of different contexts like proving the confluence of rewrite systems or analyzing the termination of narrowing. In this paper, we introduce a new technique to prove relative termination by reducing it to dependency pair problems. To the best of our knowledge, this is the first significant contribution to Problem #106 of the RTA List of Open Problems. The practical significance of our method is illustrated by means of an experimental evaluation.

We prove decidability of univariate real algebra extended with predicates for rational and integer powers, i.e., “

$$x^n \in \mathbb {Q}$$

” and “

$$x^n \in \mathbb {Z}$$

.” Our decision procedure combines computation over real algebraic cells with the rational root theorem and witness construction via algebraic number density arguments.

We present a decision procedure that combines reasoning about datatypes and codatatypes. The dual of the acyclicity rule for datatypes is a uniqueness rule that identifies observationally equal codatatype values, including cyclic values. The procedure decides universal problems and is composable via the Nelson–Oppen method. It has been implemented in CVC4, a state-of-the-art SMT solver. An evaluation based on problems generated from theories developed with Isabelle demonstrates the potential of the procedure.

We propose a tableau-based decision procedure for the full Alternating-time Temporal Logic

$$\mathsf {ATL^*}$$

. We extend our procedure for

$$\mathsf {ATL^{+}}$$

in order to deal with nesting of temporal operators. As a side effect, we obtain a new and conceptually simple tableau method for

$$\mathsf {CTL^*}$$

. The worst case complexity of our procedure is

$$\mathrm {3EXPTIME} $$

, which is suboptimal compared to the

$$\mathrm {2EXPTIME} $$

complexity of the problem. However our method is human-readable and easily implementable. A web application and binaries for our procedure are available at

http://atila.ibisc.univ-evry.fr/tableau_ATL_star/

.

Hereditarily finite (HF) set theory provides a standard universe of sets, but with no infinite sets. Its utility is demonstrated through a formalisation of the theory of regular languages and finite automata, including the Myhill-Nerode theorem and Brzozowski’s minimisation algorithm. The states of an automaton are HF sets, possibly constructed by product, sum, powerset and similar operations.

This paper describes SEPIA, a tool for automated proof generation in Coq. SEPIA combines model inference with interactive theorem proving. Existing proof corpora are modelled using state-based models inferred from tactic sequences. These can then be traversed automatically to identify proofs. The SEPIA system is described and its performance evaluated on three Coq datasets. Our results show that SEPIA provides a useful complement to existing automated tactics in Coq.

We describe an executable specification and a total correctness proof of a King and Rook vs King (KRK) chess endgame strategy within the proof assistant Isabelle/HOL. This work builds upon a previous computer-assisted correctness analysis performed using the constraint solver URSA. The distinctive feature of the present machine verifiable formalization is that all central properties have been automatically proved by the SMT solver Z3 integrated into Isabelle/HOL, after being suitably expressed in linear integer arithmetic. This demonstrates that the synergy between the state-of-the-art automated and interactive theorem proving is mature enough so that very complex conjectures from various AI domains can be proved almost in a “push-button” manner, yet in a rich logical framework offered by the modern ITP systems.

beluga

is a proof environment which provides a sophisticated infrastructure for implementing formal systems based on the logical framework LF together with a first-order reasoning language for implementing inductive proofs about them following the Curry-Howard isomorphism.

In this paper we describe four significant extensions to

beluga

: (1) we enrich our infrastructure for modelling formal systems with first-class simultaneous substitutions, a key and common concept when reasoning about formal systems (2) we support inductive definitions in our reasoning language which significantly increases

beluga

’s expressive power (3) we provide a totality checker which guarantees that recursive programs are well-founded and correspond to inductive proofs (4) we describe an interactive program development environment. Taken together these extensions enable direct and compact mechanizations. To demonstrate

beluga

’s strength and illustrate these new features we develop a weak normalization proof using logical relations.

SMTtoTPTP

is a converter from proof problems written in the SMT-LIB format into the TPTP TFF format. The SMT-LIB format supports polymorphic sorts and frequently used theories like those of uninterpreted function symbols, arrays, and certain forms of arithmetics. The TPTP TFF format is an extension of the TPTP format widely used by automated theorem provers, adding a sort system and arithmetic theories.

SMTtoTPTP

is useful for, e.g., making SMT-LIB problems available to TPTP system developers, and for making TPTP systems available to users of SMT solvers. This paper describes how the conversion works, its functionality and limitations.

In this paper we give an overview of proof-search method for CTL model checking based on Deduction Modulo. Deduction Modulo is a reformulation of Predicate Logic where some axioms—possibly all—are replaced by rewrite rules. The focus of this paper is to give an encoding of temporal properties expressed in CTL, by translating the logical equivalence between temporal operators into rewrite rules. This way, the proof-search algorithms designed for Deduction Modulo, such as Resolution Modulo or Tableaux Modulo, can be used in verifying temporal properties of finite transition systems. An experimental evaluation using Resolution Modulo is presented.

An algorithm for generating prime implicates of sets of equational ground clauses is presented. It consists in extending the standard Superposition Calculus with rules that allow attaching hypotheses to clauses to perform additional inferences. The hypotheses that lead to a refutation represent implicates of the original set of clauses. The set of prime implicates of a clausal set can thus be obtained by saturation of this set. Data structures and algorithms are also devised to represent sets of

constrained

clauses in an efficient and concise way.

Our method is proven to be correct and complete. Practical experimentations show the relevance of our method in comparison to existing approaches for propositional or first-order logic.

Monoidal algebraic structures consist of operations that can have multiple outputs as well as multiple inputs, which have applications in many areas including categorical algebra, programming language semantics, representation theory, algebraic quantum information, and quantum groups. String diagrams provide a convenient graphical syntax for reasoning formally about such structures, while avoiding many of the technical challenges of a term-based approach. Quantomatic is a tool that supports the (semi-)automatic construction of equational proofs using string diagrams. We briefly outline the theoretical basis of Quantomatic’s rewriting engine, then give an overview of the core features and architecture and give a simple example project that computes normal forms for commutative bialgebras.

This paper introduces a pseudo-concurrent architecture for first-order saturation-based theorem provers with the eventual aim of developing it into a truly concurrent architecture. The motivation behind this architecture is two-fold. Firstly, first-order theorem provers have many configuration parameters and commonly utilise multiple strategies to solve problems. It is also common that one of these strategies will solve the problem quickly but it may have to wait for many other strategies to be tried first. The architecture we propose interleaves the execution of these strategies, increasing the likeliness that these ‘quick’ proofs will be found. Secondly, previous work has established the existence of a synergistic effect when allowing proof attempts to communicate by sharing information about their inferences or clauses. The recently introduced AVATAR approach to splitting uses a SAT solver to explore the clause search space. The new architecture considers sharing this SAT solver between proof attempts, allowing them to share information about pruned areas of the search space, thus preventing them from making unnecessary inferences. Experimental results, using hard problems from the TPTP library, show that interleaving can lead to problems being solved more quickly, and that sharing the SAT solver can lead to new problems being solved by the combined strategies that were never solved individually by any existing theorem prover.

The recently developed

LowerUnits

algorithm compresses propositional resolution proofs generated by SAT- and SMT-solvers by postponing and lowering resolution inferences involving unit clauses, which have exactly one literal. This paper describes a generalization of this algorithm to the case of first-order resolution proofs generated by automated theorem provers. An empirical evaluation of a simplified version of this algorithm on hundreds of proofs shows promising results.

Beagle

is an automated theorem prover for first-order logic modulo built-in theories. It implements a refined version of the hierarchic superposition calculus. This system description focuses on

Beagle

’s proof procedure, background reasoning facilities, implementation, and experimental results.

Lean is a new open source theorem prover being developed at Microsoft Research and Carnegie Mellon University, with a small trusted kernel based on dependent type theory. It aims to bridge the gap between interactive and automated theorem proving, by situating automated tools and methods in a framework that supports user interaction and the construction of fully specified axiomatic proofs. Lean is an ongoing and long-term effort, but it already provides many useful components, integrated development environments, and a rich API which can be used to embed it into other systems. It is currently being used to formalize category theory, homotopy type theory, and abstract algebra. We describe the project goals, system architecture, and main features, and we discuss applications and continuing work.

E.T. 0.1 is a meta-system specialized for theorem proving over large first-order theories containing thousands of axioms. Its design is motivated by the recent theorem proving experiments over the Mizar, Flyspeck and Isabelle data-sets. Unlike other approaches, E.T. does not learn from related proofs, but assumes a situation where previous proofs are not available or hard to get. Instead, E.T. uses several layers of complementary methods and tools with different speed and precision that ultimately select small sets of the most promising axioms for a given conjecture. Such filtered problems are then passed to E, running a large number of suitable automatically invented theorem-proving strategies. On the large-theory Mizar problems, E.T. considerably outperforms E, Vampire, and any other prover that does not learn from related proofs. As a general ATP, E.T. improved over the performance of unmodified E in the combined FOF division of CASC 2014 by 6 %.

Modern first-order resolution and superposition theorem provers use saturation algorithms to search for a refutation in clauses derivable from the input clauses. On hard problems, this search space often grows rapidly and performance degrades especially fast when long and heavy clauses are generated. One approach that has proved successful in taming the search space is

splitting

where clauses are split into components with disjoint variables and the components are asserted in turn. This reduces the length and weight of clauses in the search space at the cost of keeping track of splitting decisions.

This paper considers the new AVATAR (Advanced Vampire Architecture for Theories And Resolution) approach to splitting which places a SAT (or SMT) solver at the centre of the theorem prover and uses it to direct the exploration of the search space. Using such an approach also allows the propositional part of the search space to be dealt with outside of the first-order prover.

AVATAR has proved very successful, especially for problems coming from applications such as program verification and program analysis as these commonly contain clauses suitable for splitting. However, AVATAR is still a new idea and there is much left to understand. This paper presents an in-depth exploration of this new architecture, introducing new, highly experimental, options that allow us to vary the operation and interaction of the various components. It then extensively evaluates these new options, using the TPTP library, to gain an insight into which of these options are essential and how AVATAR can be optimally applied.

The Nelson-Oppen combination method is ubiquitous in Satisfiability Modulo Theories solvers. However, one of its major drawbacks is to be restricted to disjoint unions of theories. We investigate the problem of extending this combination method to particular non-disjoint unions of theories connected via bridging functions. The motivation is, e.g., to solve verification problems expressed in a combination of data structures connected to arithmetic with bridging functions such as the length of lists and the size of trees. We present a sound and complete combination procedure à la Nelson-Oppen for the theory of absolutely free data structures, including lists and trees. This combination procedure is then refined for standard interpretations. The resulting theory has a nice politeness property, enabling combinations with arbitrary decidable theories of elements.

We present an approach to understanding first-order theories by exploring their models. A typical use case is the analysis of artifacts such as policies, protocols, configurations, and software designs. For the analyses we offer, users are not required to frame formal properties or construct derivations. Rather, they can explore examples of their designs, confirming the expected instances and perhaps recognizing bugs inherent in surprising instances.

Key foundational ideas include: the information preorder on models given by homomorphism, an inductively-defined refinement of the Herbrand base of a theory, and a notion of provenance for elements and facts in models. The implementation makes use of SMT-solving and an algorithm for minimization with respect to the information preorder on models.

Our approach is embodied in a tool, Razor, that is complete for finite satisfiability and provides a read-eval-print loop used to navigate the set of finite models of a theory and to display provenance.

Algorithmic deduction and abstract interpretation are two widely used and successful approaches to implementing program verifiers. A major impediment to combining these approaches is that their mathematical foundations and implementation approaches are fundamentally different. This paper presents a new, logical perspective on abstract interpreters that perform reachability analysis using non-relational domains. We encode reachability of a location in a control-flow graph as satisfiability in a monadic, second-order logic parameterized by a first-order theory. We show that three components of an abstract interpreter, the lattice, transformers and iteration algorithm, represent a first-order, substructural theory, parametric deduction and abduction in that theory, and second-order constraint propagation.

This paper introduces a new proof calculus for

differential dynamic logic

(

$$\mathsf {d}\mathcal {L}$$

) that is entirely based on

uniform substitution

, a proof rule that substitutes a formula for a predicate symbol everywhere. Uniform substitutions make it possible to rely on

axioms

rather than axiom schemata, substantially simplifying implementations. Instead of subtle schema variables and soundness-critical side conditions on the occurrence patterns of variables, the resulting calculus adopts only a finite number of ordinary

$$\mathsf {d}\mathcal {L}$$

formulas as axioms. The static semantics of differential dynamic logic is captured exclusively in uniform substitutions and bound variable renamings as opposed to being spread in delicate ways across the prover implementation. In addition to sound uniform substitutions, this paper introduces

differential forms

for differential dynamic logic that make it possible to internalize differential invariants, differential substitutions, and derivations as first-class axioms in

$$\mathsf {d}\mathcal {L}$$

.

We present an approach for component-based program synthesis that uses two distinct interpretations for the symbols in the program. The first interpretation defines the semantics of the program. It is used to specify functional requirements. The second interpretation is used to capture nonfunctional requirements that may vary by application. We present a language for program synthesis from components that uses dual interpretation. We reduce the synthesis problem to an exists-forall problem, which is solved using the exists-forall extension of the SMT-solver Yices. We use our approach to synthesize bitvector manipulation programs, padding-based encryption schemes, and block cipher modes of operations.

This paper considers Reynolds’s separation logic with all logical connectives but without arbitrary predicates. This logic is not recursively enumerable but is very useful in practice. We give a sound labelled sequent calculus for this logic. Using numerous examples, we illustrate the subtle deficiencies of several existing proof calculi for separation logic, and show that our rules repair these deficiencies. We extend the calculus with rules for linked lists and binary trees, giving a sound, complete and terminating proof system for a popular fragment called symbolic heaps. Our prover has comparable performance to Smallfoot, a prover dedicated to symbolic heaps, on valid formulae extracted from program verification examples; but our prover is not competitive on invalid formulae. We also show the ability of our prover beyond symbolic heaps, our prover handles the largest fragment of logical connectives in separation logic.

We present KeY-ABS, a tool for deductive verification of concurrent and distributed programs written in ABS. KeY-ABS allows to verify data dependent and history-based functional properties of ABS models. In this paper we give a glimpse of system workflow, tool architecture, and the usage of KeY-ABS. In addition, we briefly present the syntax, semantics and calculus of KeY-ABS Dynamic Logic (ABSDL). The system is available for download.

KeYmaera X is a theorem prover for

differential dynamic logic

(

), a logic for specifying and verifying properties of hybrid systems. Reasoning about complicated hybrid systems models requires support for sophisticated proof techniques, efficient computation, and a user interface that crystallizes salient properties of the system. KeYmaera X allows users to specify custom proof search techniques as

tactics

, execute these tactics in parallel, and interface with partial proofs via an extensible user interface.

Advanced proof search features—and user-defined tactics in particular—are difficult to check for soundness. To admit extension and experimentation in proof search without reducing trust in the prover, KeYmaera X is built up from a

small trusted kernel

. The prover kernel contains a list of sound

axioms that are instantiated using a uniform substitution proof rule. Isolating all soundness-critical reasoning to this prover kernel obviates the intractable task of ensuring that each new proof search algorithm is implemented correctly. Preliminary experiments suggest that a single layer of tactics on top of the prover kernel provides a rich language for implementing novel and sophisticated proof search techniques.

PRSPDL is a propositional dynamic logic with an operator for parallel compositions of programs. We first give a complexity upper bound for this logic. Then we focus on the class of

$$\vartriangleleft $$

-deterministic frames and give tableaux methods for two fragments of PRSPDL over this class of frames.

The second-order unification problem is undecidable. While unification procedures, like Huet’s pre-unification, terminate with success on unifiable problems, they might not terminate on non-unifiable ones. There are several decidability results for infinitary unification, such as for monadic second-order problems. These results are based on the regular structure of the solutions of these problems and by computing minimal unifiers. In this paper we describe a refinement to Huet’s pre-unification procedure for arbitrary second-order signatures which, in some cases, terminates on problems on which the original pre-unification procedure fails to terminate. We show that the refinement has, asymptotically, the same complexity as the original procedure. Another contribution of the paper is the identification of a new decidable class of second-order unification problems.

Rigid

E

-unification is the problem of unifying two expressions modulo a set of equations, with the assumption that every variable denotes exactly one term (

rigid

semantics). This form of unification was originally developed as an approach to integrate equational reasoning in tableau-like proof procedures, and studied extensively in the late 80 s and 90s. However, the fact that

simultaneous

rigid

E

-unification is undecidable has limited practical adoption, and to the best of our knowledge there is no tableau-based theorem prover that uses rigid

E

-unification. We introduce simultaneous bounded rigid

E

-unification (BREU), a new version of rigid

E

-unification that is bounded in the sense that variables only represent terms from finite domains. We show that (simultaneous) BREU is NP-complete, outline how BREU problems can be encoded as propositional SAT-problems, and use BREU to introduce a sound and complete sequent calculus for first-order logic with equality.

An effective SAT preprocessing technique is the addition of symmetry-breaking predicates: auxiliary clauses that guide a SAT solver away from needless exploration of isomorphic sub-problems. Symmetry-breaking predicates have been in use for over a decade. However, it was not known how to express the addition of these predicates in proofs of unsatisfiability. Hence, results obtained by symmetry breaking cannot be validated by existing proof checkers. We present a method to express the addition of symmetry-breaking predicates in DRAT, a clausal proof format supported by top-tier solvers. We applied this method to generate SAT problems that have not been previously solved without symmetry-breaking predicates. We validated these proofs with an ACL2-based, mechanically-verified DRAT proof checker and the proof-checking tool of SAT Competition 2014.

We present a method and an associated system, called

MathCheck

, that embeds the functionality of a computer algebra system (CAS) within the inner loop of a conflict-driven clause-learning SAT solver. SAT+CAS systems, a la

MathCheck

, can be used as an assistant by mathematicians to either counterexample or finitely verify open universal conjectures on any mathematical topic (e.g., graph and number theory, algebra, geometry, etc.) supported by the underlying CAS system. Such a SAT+CAS system combines the efficient search routines of modern SAT solvers, with the expressive power of CAS, thus complementing both. The key insight behind the power of the SAT+CAS combination is that the CAS system can help cut down the search-space of the SAT solver, by providing learned clauses that encode theory-specific lemmas, as it searches for a counterexample to the input conjecture (just like the T in DPLL(T)). In addition, the combination enables a more efficient encoding of problems than a pure Boolean representation.

In this paper, we leverage the graph-theoretic capabilities of an open-source CAS, called SAGE. As case studies, we look at two long-standing open mathematical conjectures from graph theory regarding properties of hypercubes: the first conjecture states that any matching of any d-dimensional hypercube can be extended to a Hamiltonian cycle; and the second states that given an edge-antipodal coloring of a hypercube, there always exists a monochromatic path between two antipodal vertices. Previous results have shown the conjectures true up to certain low-dimensional hypercubes, and attempts to extend them have failed until now. Using our SAT+CAS system,

MathCheck

, we extend these two conjectures to higher-dimensional hypercubes. We provide detailed performance analysis and show an exponential reduction in search space via the SAT+CAS combination relative to finite brute-force search.

We consider feasibility of linear integer programs in the context of verification systems such as SMT solvers or theorem provers. Although satisfiability of linear integer programs is decidable, many state-of-the-art solvers neglect termination in favor of efficiency. It is challenging to design a solver that is both terminating and practically efficient. Recent work by Jovanović and de Moura constitutes an important step into this direction. Their algorithm CUTSAT is sound, but does not terminate, in general. In this paper we extend their CUTSAT algorithm by refined inference rules, a new type of conflicting core, and a dedicated rule application strategy. This leads to our algorithm CUTSAT++, which guarantees termination.