Lydia G. Kondylidou

Proofs generated by resolution and superposition provers can be difficult for humans to read and understand, partly because the proofs are by contradiction, and partly because they rely on unification. We introduce a structured proof format for the Horn fragment of first-order logic with equality. The format expresses direct proofs. It combines equational rewriting chains and human-style "have/hence" derivations. It relies on matching but not full unification, increasing intelligibility. To interface with provers, we introduce an algorithm that translates resolution and superposition proofs to our format and have implemented it in a tool called Tälja. We have also connected Tälja to the Twee equational prover, which supports the Horn fragment via an encoding. We have evaluated our approach on TPTP benchmarks.

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.