Lydia Kondylidou

In the context of the Equational Theories Project, Terence Tao posed the challenge of finding alternatives to a complicated 62-step proof found by the Vampire superposition prover. We introduce a proof minimization tool called Krympa. Using a combination of brute force and heuristics, and exploiting both Vampire and the Twee equational prover, the tool reduces the 62-step proof to 20 steps, each corresponding to a rewrite. In an empirical evaluation, it also performs well on 1431 equational problems originating from the same project, reducing in particular a 151-step proof to only 10 steps.

Satisfiability modulo theories (SMT) solvers are widely used for determining the satisfiability of logical formulas with respect to back- ground theories. SMT solvers are traditionally based on first-order logic, but some also support higher-order logic. Recently, Kondylidou et al. introduced model-based quantifier instantiation with fast enumeration (MBQI-Enum), a quantifier instantiation strategy that works for both logics. A weakness of MBQI-Enum is that it does not find refutations when Hilbert choice terms are necessary. In this work, we present an extension of MBQI-Enum that enables it to reason effectively about Hilbert’s choice operator. The extended strategy substantially increases the success rate of the SMT solver cvc5 on higher-order benchmarks.

Satisfiability-modulo-theories (SMT) solvers rely on various quantifier instantiation strategies to support first- and higher-order logic. We introduce MBQI-Enum, an approach that extends model-based quan- tifier instantiation (MBQI) with syntax-guided synthesis (SyGuS) tech- niques. Our approach targets first-order theories without well-established quantifier instantiation techniques and higher-order quantifiers that can benefit from instantiations with λ-terms. By incorporating a SyGuS enu- merator, it generates a broader set of candidate instantiations, including identity functions and terms containing uninterpreted symbols, thereby improving the effectiveness of MBQI.