Vampire17: Papers with Abstracts

Abstract. In this paper we examine two cases where solutions to one system of constraints can be used or adapted to solutions to others, for free. We first revisit a method by Bromberger for lifting solutions to systems over linear real arithmetic to solutions over integers. We extend it by identifying several scenarios where solutions over reals can be directly used to establish solutions over integers. Our second case discusses model-based projection, which was introduced in two different places with different, dual, definitions. It turns out that one can typically use the same underlying engines to compute both versions of model based projection and we characterize when this is the case. We extend projection with model- based realization. When used for quantifier reasoning, it serves a complementary purpose than projection. While projection can be used for computing conflict clauses, realizers may be used for forward pruning.

Abstract. We describe a light-weight integration of the propositional SAT solver PicoSAT and the saturation-based superposition prover E. The proof search is driven by the saturation prover. Periodically, the saturation is interrupted, and all first-order clauses are grounded. The resulting ground problem is converted to a propositional format and handed to the SAT solver. If the SAT solver reports unsatisfiability, the proof is extracted and reported on the first-order level. First experiments demonstrate the viability of the approach and suggest future extensions. They also yield interesting information about the structure of the search space.

Abstract. 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.

Abstract. With first-order interpolation as the application in mind, we study the problem of gen- erating local proofs in theorem provers employing the AVATAR architecture. The theory is complemented by experimental results based on our implementation of the techniques in theorem prover Vampire.

Abstract. 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.

Abstract. Both SMT and SAT solvers can be used incrementally. This can be useful in lots of applications. Indeed, internally, Vampire uses both Minisat and Z3 incrementally. In this paper, we explore how VAMPIRE could be used incrementally. There are two forms of incremental solving. The first is where a solver is provided with formulas from a problem one by one with consistency being checked at certain points. The second more general form is where stack operations are used to create different solving contexts. We explore both ideas and show how they can be achieved within VAMPIRE. We argue that the second approach may be more suited to VAMPIRE as it allows for the incremental solving of unsatisfiable problems (whereas the first assumes a series of satisfiable problems) and the use of different solving contexts allows VAMPIRE to make use of incomplete proof search strategies. For the first approach, it will be necessary to restrict preprocessing steps to ensure completeness when additional formulas are added. For the second approach, we can make use of clauses labelled with assertions and take advantage of AVATAR to keep track of the stack information.

Abstract. Question answering is the process of taking a conjecture existentially quantified at the outer- most level and providing one or more instantiations of the quantified variable(s) as a form of an answer to the implied question. For example, given the axioms p(a) and f(a)=a the question ?[X] : p(f(X)) could return the answer X=a. This paper reviews the question answering prob- lem focussing on how it is tackled within the VAMPIRE theorem prover. It covers how VAMPIRE extracts single answers, multiple answers, disjunctive answers, and answers involving theories such as arithmetic. The paper finishes by considering possible future directions, such as integration with finite model finding.