Superposition with Lambdas

We designed a superposition calculus for a clausal fragment of extensional polymorphic higher-order logic that includes anonymous functions but excludes Booleans. The inference rules work on $$\beta \eta $$ β η -equivalence classes of $$\lambda $$ λ -terms and rely on higher-order unification to achieve refutational completeness. We implemented the calculus in the Zipperposition prover and evaluated it on TPTP and Isabelle benchmarks. The results suggest that superposition is a suitable basis for higher-order reasoning.

Model Completeness, Uniform Interpolants and Superposition Calculus

Uniform interpolants have been largely studied in non-classical propositional logics since the nineties; a successive research line within the automated reasoning community investigated uniform quantifier-free interpolants (sometimes referred to as “covers”) in first-order theories. This further research line is motivated by the fact that uniform interpolants offer an effective solution to tackle quantifier elimination and symbol elimination problems, which are central in model checking infinite state systems. This was first pointed out in ESOP 2008 by Gulwani and Musuvathi, and then by the authors of the present contribution in the context of recent applications to the verification of data-aware processes. In this paper, we show how covers are strictly related to model completions, a well-known topic in model theory. We also investigate the computation of covers within the Superposition Calculus, by adopting a constrained version of the calculus and by defining appropriate settings and reduction strategies. In addition, we show that computing covers is computationally tractable for the fragment of the language used when tackling the verification of data-aware processes. This observation is confirmed by analyzing the preliminary results obtained using the mcmt tool to verify relevant examples of data-aware processes. These examples can be found in the last version of the tool distribution.

Superposition with First-class Booleans and Inprocessing Clausification

We present a complete superposition calculus for first-order logic with an interpreted Boolean type. Our motivation is to lay the foundation for refutationally complete calculi in more expressive logics with Booleans, such as higher-order logic, and to make superposition work efficiently on problems that would be obfuscated when using clausification as preprocessing. Working directly on formulas, our calculus avoids the costly axiomatic encoding of the theory of Booleans into first-order logic and offers various ways to interleave clausification with other derivation steps. We evaluate our calculus using the Zipperposition theorem prover, and observe that, with no tuning of parameters, our approach is on a par with the state-of-the-art approach.

Prime Implicate Generation in Equational Logic (extended abstract)

A procedure is proposed to efficiently generate sets of ground implicates of first-order formulas with equality. It is based on a tuning of the superposition calculus, enriched with rules that add new hypotheses on demand during the proof search. Experimental results are presented, showing that the proposed approach is more efficient than state-of-the-art systems.

Using Vampire with Support for Algebraic Datatypes in Type Soundness Proofs

In our ongoing project VeriTaS, we aim at automating soundness proofs for type sys- tems of domain-specific languages. In the past, we successfully used previous Vampire versions for automatically discharging many intermediate proof obligations arising within standard soundness proofs for small type systems. With older Vampire versions, encoding the individual proof problems required manual encoding of algebraic datatypes via the theory of finite term algebras. One of the new Vampire versions now supports the direct specification of algebraic datatypes and integrates reasoning about term algebras into the internally used superposition calculus.In this work, we investigate how many proof problems that typically arise within type soundness proofs different Vampire 4.1 versions can prove. Our test set consists of proof problems from a progress proof of a type system for a subset of SQL. We compare running Vampire 4.1 with our own encodings of algebraic datatypes (in untyped as well as in typed first-order logic) to running Vampire 4.1 with support for algebraic datatypes, which uses SMTLIB as input format. We observe that with our own encodings, Vampire 4.1 still proves more of our input problems. We discuss the differences between our own encoding of algebraic datatypes and the ones used within Vampire 4.1 with support for algebraic datatypes.

An Inference Rule for the Acyclicity Property of Term Algebras

Term algebras are important structures in many areas of mathematics and computer science. Reasoning about their theories in superposition-based first-order theorem provers is made difficult by the acyclicity property of terms, which is not finitely axiomatizable. We present an inference rule that extends the superposition calculus and allows reasoning about term algebras without axioms to describe the acyclicity property. We detail an indexing technique to efficiently apply this rule in problems containing a large number of clauses. Finally we experimentally evaluate an implementation of this extended calculus in the first-order theorem prover Vampire. The results show that this technique is able to find proofs for difficult problems that existing SMT solvers and first-order theorem provers are unable to solve.

First-Order Interpolation and Interpolating Proof Systems

It is known that one can extract Craig interpolants from so-called localproofs. An interpolant extracted from such a proof is a booleancombination of formulas occurring in the proof. However, standard completeproof systems, such as superposition, for theories having the interpolationproperty are not necessarily complete for local proofs: there are formulashaving non-local proofs but no local proof.In this paper we investigate interpolant extraction from non-local refutations(proofs of contradiction) in the superposition calculus and prove a numberof general results about interpolant extraction and complexity of extractedinterpolants. In particular, we prove that the number of quantifier alternationsin first-order interpolants of formulas without quantifier alternations isunbounded. This result has far-reaching consequences for using local proofsas a foundation for interpolating proof systems: any such proof system shoulddeal with formulas of arbitrary quantifier complexity.To search for alternatives for interpolating proof systems, we consider severalvariations on interpolation and local proofs. Namely, we give an algorithm forbuilding interpolants from resolution refutations in logic without equality anddiscuss additional constraints when this approach can be also used for logicwith equality. We finally propose a new direction related to interpolation vialocal proofs in first-order theories.

A Clausal Normal Form Translation for FOOL

Automated theorem provers for first-order logic usually operate on sets of first-order clauses. It is well-known that the translation of a formula in full first-order logic to a clausal normal form (CNF) can crucially affect performance of a theorem prover. In our recent work we introduced a modification of first-order logic extended by the first class boolean sort and syntactical constructs that mirror features of programming languages. We called this logic FOOL. Formulas in FOOL can be translated to ordinary first-order formulas and checked by first-order theorem provers. While this translation is straightforward, it does not result in a CNF that can be efficiently handled by state-of-the-art theorem provers which use superposition calculus. In this paper we present a new CNF translation algorithm for FOOL that is friendly and efficient for superposition-based first-order provers. We implemented the algorithm in the Vampire theorem prover and evaluated it on a large number of problems coming from formalisation of mathematics and program analysis. Our experimental results show an increase of performance of the prover with our CNF translation compared to the naive translation.