Saturation-Guided Inductive Synthesis

SAT in Saturation: A Satisfied Match

A tailored integration of SAT solving for detecting variants of subsumption in superposition using the Vampire prover and showing that SAT encodings improve literal matching, and thus subsumption, in first-order theorem proving is presented.

Interactive Proofs in Higher-Order Logic with Errors and Application to Concrete Cryptography

Computer-aided cryptography (CAC) provides strong guarantees through mechanized proofs of security. SquirREL is a proof assistant specialized in CAC, but is restricted to the asymptotic setting, which limits its applicability. Recent theoretical work [1] adapted Squirrel’s underlying logic to the concrete setting through the introduction of a higher-order logic with errors. While this allows to prove precise security bounds on paper, it only provides a low-level logical calculus which lacks an implementation. Thus, it falls short of the CAC aims.In this paper, we use this low-level calculus to build the full-fledged set of features used in a proof assistant such as Squirrel, with a focus on reachability reasoning. We design higher-level logical mechanisms on top of this logic, including proof context management, introduction patterns, and boundannotated tactics. To do so, we introduce a proof term calculus with dedicated features for bounds, for which we design an elaborator. This elaborator can automatically infer bound-related manipulations, improving usability and reducing user inputs, and we theoretically argue for its usability through an erasability theorem. All these improvements have been implemented as an extension of Squirrel, and we provide empirical evidence of the applicability of our framework through case studies.

Proof-Relevant Interpolation: Beyond Cut-Free and Sequent Proofs

Beyond Core-Guided MaxSAT

A new proof system for MaxSAT is described, the Comparator Calculus, which models the inferential strategies used in core-guided MaxSAT solvers and two new MaxSAT algorithms are introduced: a core-guided one (CSimple) and one non-core-guided (CSat), which uses heuristics to construct new soft formulas and calls a SAT solver on a single soft formula.

Proof Production for Satisfiability Modulo Finite Fields with Proof Checking in Pacheck and Lean

Conflict-Driven SAT Solving using XOR-OR-AND Normal Forms

Solving Boolean polynomial systems, or equivalently, SAT-solving, based on the XNF and the XLIN proof system outperforms classical methods not only theoretically, but based on the new conflict-driven XNF clause learning methods developed here, it is possible to implement an XNF solver with good practical efficiency.