The Next Generation of Deduction Systems: From Composition to Compositionality

In this short presentation, essentially meant to stimulate the discussion among participants, I exposed a very subjective view on the evolution of automated reasoning software, from many small one-person projects in the 90s to a few huge tools now. This poses a problem for the future of the field. I advocate a modular approach to software in our field, to enable reuse, for better distribution of the work, for students to more easily understand the tools by parts, and for better evaluation of parts of automated reasoning software. I briefly reported on my first experiment for a modular approach in SMT with modulariT.

In this talk, we first review basic correspondences between syntactic interpolation properties of a first order theory (quantifier-free interpolation property, general quantifier-free interpolation property, uniform quantifier-free interpolation property) and semantic features related to the class of its models (amalgamation, strong amalgamation, model completability). Then we shall analyze these notions for variants of McCarthy extensional theory of arrays. Whereas the basic theory does not have quantifier-free interpolation property, such property can be restored by adding it an extra symbol ‘diff’ skolemizing the extensionality axiom. General quantifier-free interpolation property also holds for this theory but not uniform quantifier-free interpolation property, as shown by an explicit counterexample. Since the semantic content of diff operation is rather underspecified, we strenghten the theory by asking diff(a,b) to return the maximum index where two arrays a,b differ (diff returns 0 if they are equal). We also add to a unary ‘length’ operation. We so end up in a theory still having quantifier-free interpolation, as witnessed by a hyerarchic polynomial reduction to general interpolation for linear arithmetics over indexes. General quantifier free interpolation property may fail, but can be re-gained by introducing constant arrays.

The second part of this talk comes from joint work with A. Gianola, D. Kapur, C. Naso [ACM-TOCL, October 2023]. The first part of the talk reviews old joint work with R. Bruttomesso and S. Ranise, adding to such old work some recent achievements.

Traditional finance is largely based on the assumption that human actors behave in a trustworthy manner. When this trust was misplaced, this has resulted in big losses for financial systems. Decentralized finance (DeFi) provides a solution by making financial protocols transparent and automated. As a result DeFi does not have the guardrails provided by humans, and catastrophic failures result from incorrect implementations. Certora’s bounded model checking based tool helps finding faults in the protocols in an exhaustive way. In this talk I describe how a critical bug was found and fixed in a protocol design and how the tool helped in this process.

In this talk, we would like to introduce some new approaches to solving the SMT problem, including: 1. A bit-blasting based algorithm for SMT(NIA) formulas; 2. A gradient-based algorithm for SMT(NRA) formulas; 3. SMT solving under probability distribution. These works explored the advancement of four components of SMT solving: Search Space Allocation, Variable Order Selection, Model or Partial Model Generation, and Value Decision.

Logically Constrained Term Rewriting Systems offer a way to couple traditional reasoning on term rewriting systems with SMT reasoning (and tools). This allows them, in turn, to be used for program analysis in a more natural way than pure rewriting (and in different ways than pure SMT). But to model functional languages naturally, we should ideally combine higher-order term rewriting systems with SMT. In this presentation, I will discuss the choices to be made for that goal.

The proof assistant Isabelle/HOL can call external solvers to automate proof search, which is crucial for using it more effectively. In particular, statements containing bit-vectors are notoriously tedious to prove manually. cvc5 is an efficient satisfiability modulo theories (SMT) solver that is currently only indirectly used by Isabelle. The process of finding a proof inside of Isabelle with the information provided by cvc5 is slow and often fails. In this work we extend the integration between Isabelle and cvc5 so that a proof certificate from cvc5 is shared with Isabelle that can be reconstructed internally into native Isabelle/HOL proofs. We present our ongoing effort to reconstruct these proofs, including problems containing bit-vectors whose reconstruction in Isabelle is currently not supported by any other SMT solver. Modern SMT solvers implement hundreds of term rewriting rules. cvc5 is able to output fine-grained proofs using a separate database of rewrite rules written in the RARE language. We also present IsaRARE, a plugin for Isabelle, that translates such rules to lemmas in Isabelle that can then be used in the reconstruction process out of the box. Additionally, IsaRARE can be used as a verifier for rewrite rules. We evaluate our approach by verifying an extensive set of rewrite rules used by the cvc5 SMT solver.

Symbolism and connectionism are two fundamental paradigms for artificial intelligence. In the past decade, connectionism has revived in the name of deep learning, achieving great success in many areas. Recently, neuro-symbolic methods, aiming to bridge the gap between connectionism and symbolism, receive much attention. In this talk, we will introduce some of our initial efforts in this area, which can be classified into two categories: 1. The end-to-end approach where a neural network takes as input the reasoning task and directly outputs the result; 2. The composition of neural network and symbolic method, where a neural network provides assistance to the reasoning algorithm. The targeted reasoning problems include pseudo-Boolean constraint solving, MaxSAT and cylindrical algebraic decomposition.

Cylindrical algebraic decomposition (CAD) is the only complete method implemented in Satisfiability-modulo-theories solvers for solving non-linear arithmetic. Due to its doubly exponential complexity, modern algorithms compute only parts of its projection operation, making solving some practical instances of NRA tractable. There is a variety of cases where savings in the projection are possible, and often there are multiple alternatives for the projection. To manage the maintainability of an algorithm when incorporating special cases, we developed a proof system for modern CAD-based SMT algorithms. This proof system is extensible, separates heuristic decisions (which projection to take) from the correctness of the projection and can be employed in different algorithms. Further, the proof system could be a step towards formal proofs for real algebra.

We give a brief overview of VeriPB, a proof system based on pseudo-Boolean reasoning with 0-1 integer linear inequalities that seems well suited to provide a unified proof logging method for discrete combinatorial problems. We have implemented VeriPB proof logging, together with efficient proof checking, for state-of-the-art solvers in Boolean satisfiable (SAT) solving, SAT-based optimization, graph solving, constraint programming, and a growing list of other combinatorial solving paradigms. We believe that ideas from VeriPB could be useful also in the context of mixed integer linear programming and satisfiability modulo theories (SMT) solving.

This is based on joint work with Bart Bogaerts, Stephan Gocht, Ciaran McCreesh, Magnus O. Myreen, Andy Oertel, and Yong Kiam Tan.

The Tetrapod model organizes mathematical knowledge into 4+1 aspects, visualized as the corners and the center of a tetrahedral shape. The corners represent fundamentally different ways of assigning semantics, each with an ecosystem of highly specialized tools and large libraries:

• $\mathrm{■}$

  Deduction: proofs, especially if formalized and mechanically verified in proof assistants

• $\mathrm{■}$

  Computation: algorithms, especially if executably implemented in programming languages and computer algebra systems

• $\mathrm{■}$

  Tabulation: systematic lists of examples, especially if encoded as concrete objects stored in databases

• $\mathrm{■}$

  Documentation: human-readable narrative explanations, especially if systematically structured and annotated to enable machine processing

A key novelty of the model is to identify as the central aspect the intersection of the above, called Ontology: names, types, definitions, notations, and properties of mathematical objects, i.e., the information that is critical for knowledge exchange between the dedicated software systems for the other aspects.

This talk gives a high-level overview of the model in discussion-starter style and can be seen as a position statement that next generation systems must invent fundamentally new designs to fully utilize the combination of all aspects.

Satisfiability Modulo Theories (SMT) solvers are a critical component of many formal methods applications, including for software verification and security analysis. Their soundness is of the utmost importance. While SMT solvers are highly complex systems, some modern SMT solvers now are capable of generating externally checkable proofs. This talk gives the current state of proofs in the SMT solver cvc5. We introduce AletheLF, the new standard format for proofs generated by cvc5. AletheLF is a logical framework based on the SMT-LIB version 3.0 language. It combines the benefits of several previous proof efforts, including a clean syntax, extensibility and integration with other proof formats like DRAT via the use of oracles. We present an initial evaluation of AletheLF, showing the viability of performant proof generation and checking for SMT.

Unlike automated reasoning, human reasoning does not adhere to logical rules exclusively. This is also reflected in the observation of Kahneman that the human mind seems to be based on two integrated systems: a System 1 that works quickly and unconsciously, and a System 2 that works slowly and calculates logically. System 1 embodies intuitions and fast reactions to sensory signals, while System 2 represents deliberate thinking and abstract problem solving. It can be seen as a strength humans have that we have these two very different systems which we are able to combine. And in fact these two systems complement each other very nicely. Hence, the combination of statistical procedures and logical reasoning holds promise for automated reasoning. The meaning of words, like they are captured in Word Embeddings constitutes an important source of information for automated reasoning systems. In knowledge bases where predicate and function symbols align closely with words, these Word Embeddings can be employed. In previous studies, we have demonstrated the successful integration of word similarities into the selection process, where relevant knowledge for a specific query needs to be extracted from a large knowledge base. Additionally, we incorporated Word Embeddings into the selection of the given clause in the given clause algorithm within resolution provers. Initial experimental results indicate that integrating word similarities leads to provers deriving fewer resolvents and maintaining a more focused approach to the query context.

Quantified Boolean Formulas (QBFs) extend propositional logic by quantifiers over the Boolean variables. As a consequence of having quantifiers, the decision problem of QBF is PSPACE-complete. There is a symmetry between models of true QBFs and counter-models of false QBFs. Both can be represented as binary trees or as sets of Boolean functions, encoding the solutions of application problems that have been translated to QBFs. In practice, those solutions are often extracted from proofs as produced by the QBF solvers.

The landscape of QBF solving paradigms rather heterogeneous, resulting in solvers are based on various proof systems of different strength. In this talk, we review three different proof systems on which recent solvers are built. In particular, we consider Q-resolution for true and false formulas as found in QCDCL, forall-Exp Res as implemented in expansion-based systems as well as QRAT that was developed for recent pre- and inprocessing techniques.

Equational theorem provers based on Knuth-Bendix completion can solve difficult reasoning problems in, for example, algebra. But the expressive power is limited by the lack of logical connectives. I show that a completion-based prover can reason about practical problems involving connectives with the help of a SAT solver and efficient encodings. I also argue that completion is a useful setting for studying problems in saturation provers, such as how to reason in a goal-directed manner, an important but under-studied problem.

We present past and current work on hierarchical symbol elimination.
We first present a goal-oriented symbol elimination method which, given (i) a base theory ${𝒯}_0$ allowing quantifier elimination, (ii) an extension ${𝒯}_1$ of ${𝒯}_0$ with additional function symbols whose properties are axiomatised by a set $𝒦$ of clauses, (iii) a subset of the additional functions which are considered to be parameters, and (iv) a set $G$ of ground clauses, such that ${𝒯}_1\wedge G$ is satisfiable, computes a universal formula $\mathrm{\Gamma }$ containing symbols in the base theory ${𝒯}_0$ and parameters such that ${𝒯}_1\wedge \mathrm{\Gamma }\wedge G$ is unsatisfiable. The computation of $\mathrm{\Gamma }$ is done in a hierarchical way, and relies on methods for quantifier elimination in ${𝒯}_0$. We identify situations under which the formula $\mathrm{\Gamma }$ computed with our method is the weakest universal formula with the property above, and explain how we used this method for the verification of parametric systems:

1. 1.

   for generating (weakest) constraints on parameters under which certain properties are guaranteed to be inductive invariants,

2. 2.

   for iteratively strengthening properties to obtain inductive invariants.

We then briefly present a method for general symbol elimination which uses a constraint resolution calculus obtained from specializing the hierarchical superposition calculus, and explain how we used it – together with goal-oriented symbol elimination – in problems from wireless research theory.

The talk reports on an exploration of Boolos’ Curious Inference, using higher-order automated theorem provers (ATPs). Surprisingly, only suitable shorthand notations had to be provided by hand for ATPs to find a short proof. The higher-order lemmas required for constructing a short proof are automatically discovered by the ATPs. Given the observations and suggestions in this paper, full proof automation of Boolos’ and related examples now seems to be within reach of higher-order ATPs. Preliminary work on automating the synthesis of such shorthand notations is briefly presented.

The talk is based on joint work with Chris Benzmüller, David Fuenmayor and Geoff Sutcliffe [1].

This talk describes the (new) TPTP World format for representing Tarskian and Kripke interpretations of formulae in classical (FOF, TFF, TXF, THF) and non-classical (NXF, NHF) logics. A technique and implemented tool for verifying models, and a tool for visualizing Tarskian interpretations, are presented. This work provides TPTP World standards that allow interpretations to be shared between components of complex compositional reasoning systems.

In this talk, I present the current state of the Isabelle/HOL mechanization efforts by Ghilain Bergeron and myself of the splitting framework by Gabriel Ebner, Jasmin Blanchette and myself. These results include the splitting calculus from section 3 of the framework as well as a partial instance of splitting without backtracking over resolution in FOL. There is still one assumption of this instantiation that is not discharged: the compactness of FOL. Surprisingly, we were unable to find this folklore result in Isabelle/HOL already. I also present the mechanization of this result in Isabelle/HOL via Los’s theorem and explain why it is not (yet) usable to discharge the desired assumption of the splitting instance. Finally, I discuss other leads to reach this desired result.

Bachmair’s and Ganzinger’s abstract redundancy concept for the Superposition Calculus justifies almost all operations that are used in superposition provers to delete or simplify clauses, and thus to keep the clause set manageable. Typical examples are tautology deletion, subsumption deletion, and demodulation, and with a more refined definition of redundancy joinability and connectedness can be covered as well. The notable exception is destructive equality resolution, that is, the replacement of a clause $x\not\approx t\vee C$ with $x\notin \mathrm{𝑣𝑎𝑟𝑠}(t)$ by $C\{x\mapsto t\}$. This operation is implemented in state-of-the-art provers, and it is useful in practice, but little is known about how it affects refutational completeness. We demonstrate on the one hand that the naive addition of destructive equality resolution to the standard abstract redundancy concept renders the calculus refutationally incomplete. On the other hand, we present several restricted variants of the superposition calculus that are refutationally complete even with destructive equality resolution.

The talk includes an introduction to the SCL calculus, in particular its version for first-order logic. In addition, I discuss implementation aspects, in particular lifting the CDCL 2-Watched Literal Scheme to first-order logic.