Abstract Deciding the satisfiability of formulas involving both quantifiers and theory defined symbols is a challenge in automated reasoning. This article presents an algorithm, called $$\textsf{QSMA}$$ QSMA (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 $$\textsf{OptiQSMA}$$ OptiQSMA is also described and shown to preserve both partial correctness and termination. $$\textsf{OptiQSMA}$$ OptiQSMA is implemented in the YicesQS solver. $$\textsf{OptiQSMA}$$ OptiQSMA 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 ( $$\textsf{LRA}$$ LRA —Linear Rational Arithmetic, $$\textsf{LIA}$$ LIA —Linear Integer Arithmetic, $$\textsf{NRA}$$ NRA —Nonlinear Real Arithmetic, and $$\textsf{NIA}$$ NIA —Nonlinear Integer Arithmetic) and in the theory of bitvectors ( $$\textsf{BV}$$ BV ) is included.

Abstract This paper presents and proves totally correct a new algorithm, called $$\textsf{QSMA}$$ QSMA , for the satisfiability of a quantified formula modulo a complete theory and an initial assignment. The optimized variant of $$\textsf{QSMA}$$ 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 $$\textsf{LIA}$$ LIA , $$\textsf{NIA}$$ NIA , $$\textsf{LRA}$$ LRA , $$\textsf{NRA}$$ NRA , and $$\textsf{BV}$$ BV categories and ranked second for the “largest contribution” award (single queries). It was the only solver to solve all $$\textsf{LRA}$$ LRA instances, where it was about two orders of magnitude faster than the second best solver (Z3).

Abstract 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 theset-of-support strategyfor resolution theorem proving, and thedemodulationandparamodulationinference 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.

Abstract 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-drivenprocedures 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 inunions of theories. It combines inference systems for individual theories astheory moduleswithin a solver for the union of the theories. This article augments CDSAT with a more generallemma learningcapability and withproof generation. Furthermore, theory modules for several theories of practical interest are shown to fulfill the requirements forcompletenessandterminationof CDSAT. Proof generation is accomplished by aproof-carryingversion of the CDSAT transition system that producesproof objectsin memory accommodating multiple proof formats. Alternatively, one can apply to CDSAT theLCF approach to proofsfrom interactive theorem proving, by defining a kernel of reasoning primitives that guarantees the correctness by construction of CDSAT proofs.

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.

This article is a survey of recent results, related works and new challenges in automated theorem proving for program checking. The aim is to give some historical perspective, albeit necessarily incomplete, and highlight some of the turning points that made crucial advances possible.

Program analysis and verification require decision procedures to reason on theories of data structures. Many problems can be reduced to the satisfiability of sets of ground literals in theory T . If a sound and complete inference system for first-order logic is guaranteed to terminate on T-satisfiability problems , any theorem-proving strategy with that system and a fair search plan is a T-satisfiability procedure . We prove termination of a rewrite-based first-order engine on the theories of records , integer offsets , integer offsets modulo and lists . We give a modularity theorem stating sufficient conditions for termination on a combination of theories , given termination on each. The above theories, as well as others, satisfy these conditions. We introduce several sets of benchmarks on these theories and their combinations, including both parametric synthetic benchmarks to test scalability , and real-world problems to test performances on huge sets of literals. We compare the rewrite-based theorem prover E with the validity checkers CVC and CVC Lite. Contrary to the folklore that a general-purpose prover cannot compete with reasoners with built-in theories, the experiments are overall favorable to the theorem prover, showing that not only the rewriting approach is elegant and conceptually simple, but has important practical implications.

Verification problems require to reason in theories of data structures and fragments of arithmetic. Thus, decision procedures for such theories are needed, to be embedded in, or interfaced with, proof assistants or software model checkers. Such decision procedures ought to be sound and complete, to avoid false negatives and false positives, efficient, to handle large problems, and easy to combine, because most problems involve multiple theories. The rewrite-based approach to decision procedures aims at addressing these sometimes conflicting issues in a uniform way, by harnessing the power of general first-order theorem proving. In this article, we generalize the rewrite-based approach from deciding the satisfiability of sets of ground literals to deciding that of arbitrary ground formulæ in the theory. Next, we present polynomial rewrite-based satisfiability procedures for the theories of records with extensionality and integer offsets. The generalization of the rewrite-based approach to arbitrary ground formulæ and the polynomial satisfiability procedure for the theory of records with extensionality use the same key property—termed variable-inactivity—that allows one to combine theories in a simple way in the rewrite-based approach.

An abstract framework of canonical inference is used to explore how different proof orderings induce different variants of saturation and completeness. Notions like completion, paramodulation, saturation, redundancy elimination, and rewrite-system reduction are connected to proof orderings. Fairness of deductive mechanisms is defined in terms of proof orderings, distinguishing between (ordinary) “fairness,” which yields completeness, and “uniform fairness,” which yields saturation.

This paper describes a methodology for parallel theorem proving in a distributed environment, called deduction by Clause-Diffusion. This methodology utilizes parallelism at the search level, by having concurrent, asynchronous deductive processes sear