Most SMT instances involve symbols from more than one theory. The equality sharing method for combining theory satisfiability procedures has been a standard for over forty years. For the Boolean part, the equality sharing method is interfaced with the CDCL procedure for SAT. CDCL guides the search by learning lemmas from conflicts between clauses and candidate model. In the standard integration of CDCL and equality sharing, the conflict-driven reasoning remains propositional, even if conflict-driven theory procedures exist. The MCSAT method integrates CDCL with a single conflict-driven theory procedure. The CDSAT method generalizes CDCL, MCSAT, and equality sharing, by allowing the integration of multiple (conflict-driven or not) theory procedures.

Deciding the satisfiability of formulas involving both quantifiers and theory defined symbols is a challenge in automated reasoning. This article presents an algorithm, called (Quantified Satisfiability Modulo Assignment), for the satisfiability of an arbitrary quantified formula modulo a complete theory and an initial assignment. The algorithm is proved partially correct and terminating, so that its total correctness is established. An optimized variant called is also described and shown to preserve both partial correctness and termination. is implemented in the YicesQS solver. enabled YicesQS to achieve top of the line results, especially in linear rational arithmetic, in the 2022, 2023, and 2024 editions of the International Satisfiability Modulo Theories Competition (SMT-COMP). A report on these results in four fragments of arithmetic ( —Linear Rational Arithmetic, —Linear Integer Arithmetic, —Nonlinear Real Arithmetic, and —Nonlinear Integer Arithmetic) and in the theory of bitvectors ( ) is included.

The main topic of this article are SGGS decision procedures for fragments of first-order logic without equality. SGGS ( Semantically-Guided Goal-Sensitive reasoning) is an attractive basis for decision procedures, because it generalizes to first-order logic the Conflict-Driven Clause Learning (CDCL) procedure for propositional satisfiability. As SGGS is both refutationally complete and model-complete in the limit, SGGS decision procedures are model-constructing . We investigate the termination of SGGS with both positive and negative results: for example, SGGS decides Datalog and the stratified fragment (including Effectively PRopositional logic ) that are relevant to many applications. Then we discover several new decidable fragments , by showing that SGGS decides them. These fragments have the small model property , as the cardinality of their SGGS-generated models can be upper bounded, and for most of them termination tools can be applied to test a set of clauses for membership. We also present the first implementation of SGGS —the Koala theorem prover—and we report on experiments with Koala.

Automated reasoning is a key enabling technology for formal methods. Automated theorem provers (ATP) for first-order and lately higher-order logic and solvers for satisfiability modulo theories (SMT) showcase impressive power and amazing sophistication. However, ATP systems reason well about formulas with arbitrary quantification and free symbols, while SMT solvers reason well about ground formulas with defined symbols. Since formulas from applications involve both quantifiers and defined symbols, a hiatus remains open. QSMA is a new algorithm for quantifiers in SMT [4]. QSMA stands for Quantified Satisfiability Modulo theory and Assignment. Currently, QSMA works for one theory with a unique intended model, so that models differ only in the assignment of values to variables. QSMA accepts arbitrary formulas, viewing all quantifiers as existential by double negation. Since QSMA operates a recursive descent over the tree structure of the formula, peeling off quantifiers and instantiating variables, each call works modulo an assignment. By building under- and over-approximations of the formula, QSMA zooms in on a model or finds that none exists. The implementation of QSMA in the YicesQS solver [6] built on top of the Yices 2 solver [5] exhibited excellent performances in linear rational arithmetic and nonlinear arithmetic [4]. Integrating QSMA in the CDSAT framework for conflict-driven satisfiability in a union of theories [1]–[3] is the next challenge.

This paper presents and proves totally correct a new algorithm, called QSMA , for the satisfiability of a quantified formula modulo a complete theory and an initial assignment. The optimized variant of QSMA implemented in YicesQS is described and shown to preserve total correctness. A report on the performance of YicesQS at the 2022 SMT competition is included. YicesQS ran in the LIA , NIA , LRA , NRA , and BV categories and ranked second for the “largest contribution” award (single queries). It was the only solver to solve all LRA instances, where it was about two orders of magnitude faster than the second best solver (Z3).

Search-based satisfiability procedures try to build a model of the input formula by simultaneously proposing candidate models and deriving new formulae implied by the input. Conflict-driven procedures perform non-trivial inferences only when resolving conflicts between formulæ and assignments representing the candidate model. CDSAT (Conflict-Driven SATisfiability) is a method for conflict-driven reasoning in unions of theories. It combines inference systems for individual theories as theory modules within a solver for the union of the theories. This article augments CDSAT with a more general lemma learning capability and with proof generation. Furthermore, theory modules for several theories of practical interest are shown to fulfill the requirements for completeness and termination of CDSAT. Proof generation is accomplished by a proof-carrying version of the CDSAT transition system that produces proof objects in memory accommodating multiple proof formats. Alternatively, one can apply to CDSAT the LCF approach to proofs from interactive theorem proving, by defining a kernel of reasoning primitives that guarantees the correctness by construction of CDSAT proofs.

This issue collects papers written in memory of the late Larry Wos, exceptional scientist and charismatic leader during six decades of research in automated reasoning.Larry Wos was one of the founders of the field of automated reasoning, and he was the founder and the first editor-in-chief of the Journal of Automated Reasoning.The first paper in the issue, entitled "Larry Wos -Visions of Automated Reasoning," by

This article is a tribute to the scientific legacy of automated reasoning pioneer and JAR founder Lawrence T. (Larry) Wos. Larry’s main technical contributions were the set-of-support strategy for resolution theorem proving, and the demodulation and paramodulation inference rules for building equality into resolution. Starting from the original definitions of these concepts in Larry’s papers, this survey traces their evolution, unearthing the often forgotten trails that connect Larry’s original definitions to those that became standard in the field.

CDSAT ( Conflict-Driven Satisfiability ) is a paradigm for theory combination that works by coordinating theory modules to reason in the union of the theories in a conflict-driven manner. We generalize CDSAT to the case of nondisjoint theories by presenting a new CDSAT theory module for a theory of arrays with abstract length , which is an abstraction of the theory of arrays with length . The length function is a bridging function as it forces theories to share symbols, but the proposed abstraction limits the sharing to one predicate symbol. The CDSAT framework handles shared predicates with minimal changes, and the new module satisfies the CDSAT requirements, so that completeness is preserved.

This paper celebrates the scientific discoveries and the service to the automated reasoning community of Lawrence (Larry) T. Wos, who passed away in August 2020. The narrative covers Larry’s most long-lasting ideas about inference rules and search strategies for theorem proving, his work on applications of theorem proving, and a collection of personal memories and anecdotes that let readers appreciate Larry’s personality and enthusiasm for automated reasoning.

SGGS ( Semantically-Guided Goal-Sensitive reasoning) is a refutationally complete theorem-proving method that offers first-order conflict-driven reasoning and is model complete in the limit . This paper investigates the behavior of SGGS on Horn clauses , which are widely used in declarative programming, knowledge representation, and verification. We show that SGGS generates the least Herbrand model of a set of definite clauses, and that SGGS terminates on Horn clauses if and only if hyperresolution does , with the advantage that SGGS builds a model. We report on experiments applying the SGGS prototype prover Koala to Horn problems, with promising performances especially on satisfiable inputs.

The main ideas in the CDSAT (Conflict-Driven Satisfiability) framework for SMT are summarized, leading to approaches to proof generation in CDSAT.

SGGS (Semantically-Guided Goal-Sensitive reasoning) is a conflict-driven first-order theorem-proving method which is refutationally complete and model complete in the limit. These features make it attractive as a basis for decision procedures. In this paper we show that SGGS decides the stratified fragment which generalizes EPR, the PVD fragment, and a new fragment that we dub restrained. The new class has the small model property, as the size of SGGS-generated models can be upper-bounded, and is also decided by hyperresolution and ordered resolution. We report on experiments with a termination tool implementing a restrainedness test, and with an SGGS prototype named Koala.

Many applications depend on solving the satisfiability of formulæ involving propositional logic and first-order theories, a problem known as Satisfiability Modulo Theory. This article presents a new method for satisfiability modulo a combination of theories, named CDSAT, for Conflict-Driven SATisfiability. CDSAT also solves Satisfiability Modulo Assignment problems that may include assignments to first-order terms. A conflict-driven procedure assigns values to variables to build a model, and performs inferences on demand in order to solve conflicts between assignments and formulæ. CDSAT extends this paradigm to generic combinations of disjoint theories, each characterized by a collection of inference rules called theory module. CDSAT coordinates the theory modules in such a way that the conflict-driven reasoning happens in the union of the theories, not only in propositional logic. As there is no fixed hierarchy with propositional logic at the center and the other theories as satellites, CDSAT offers a flexible framework for model search. We prove the soundness, completeness, and termination of CDSAT, identifying sufficient requirements on theories and modules that ensure these properties.

Satisfiability is the problem of deciding whether a formula has a model. Although it is not even semidecidable in first-order logic, it is decidable in some first-order theories or fragments thereof (e.g., the quantifier-free fragment). Satisfiability modulo a theory is the problem of determining whether a quantifier-free formula admits a model that is a model of a given theory. If the formula mixes theories, the considered theory is their union, and combination of theories is the problem of combining decision procedures for the individual theories to get one for their union. A standard solution is the equality-sharing method by Nelson and Oppen, which requires the theories to be disjoint and stably infinite. This paper surveys selected approaches to the problem of reasoning in the union of disjoint theories, that aim at going beyond equality sharing, including: asymmetric extensions of equality sharing, where some theories are unrestricted, while others must satisfy stronger requirements than stable infiniteness; superposition-based decision procedures; and current work on conflict-driven satisfiability (CDSAT).

Search-based satisfiability procedures try to construct a model of the input formula by simultaneously proposing candidate models and deriving new formulae implied by the input. When the formulae are satisfiable, these procedures generate a model as a witness. Dually, it is desirable to have a proof when the formulae are unsatisfiable. Conflict-driven procedures perform nontrivial inferences only when resolving conflicts between the formulae and assignments representing the candidate model. CDSAT (Conflict-Driven SATisfiability) is a method for conflict-driven reasoning in combinations of theories. It combines solvers for individual theories as theory modules within a solver for the union of the theories. In this paper we endow CDSAT with lemma learning and proof generation. For the latter, we present two techniques. The first one produces proof objects in memory: it assumes that all theory modules produce proof objects and it accommodates multiple proof formats. The second technique adapts the LCF approach to proofs from interactive theorem proving to conflict-driven SMT-solving and theory combination, by defining a small kernel of reasoning primitives that guarantees that CDSAT proofs are correct by construction.