Abstract The superposition calculus for reasoning in first-order logic with equality relies on simplification orderings on terms. Modern saturation provers use the Knuth-Bendix order (KBO) and the lexicographic path order (LPO) for discovering redundant clauses and inferences. Implementing term orderings is, however, challenging. While KBO comparisons can be performed in linear time and LPO checks in quadratic time, using the best-known algorithms for these orders is not enough. Indeed, our experiments show that for some examples, term ordering checks may use about 98% of the overall proving time. The reason for this is that some equalities that cannot be ordered can become ordered after applying a substitution (post-ordered), and we have to check for post-ordering repeatedly for the same equalities. In this paper, we show how to improve post-ordering checks by introducing a new data structure called term ordering diagrams , in short TODs, which creates an index for these checks. We achieve efficiency by lazy modifications of the index and by storing and reusing information from previously performed checks to speed up subsequent checks. Our experiments demonstrate the efficiency of TODs.

Abstract Redundancy elimination is one of the crucial ingredients of efficient saturation-based proof search. We strengthen redundancy elimination by introducing a new notion of redundancy, based on partial clauses and redundancy formulas . The new notion allows us to recognize redundant clauses and inferences that cannot be recognized by standard redundancy elimination criteria. In a way, our notion blurs the distinction between redundancy at the level of inferences and redundancy at the level of clauses. We present a superposition calculus PaRC on partial clauses and prove that it is refutationally complete. We discuss the implementation of the calculus in the theorem prover Vampire . Our experiments show the power of the new approach: we were able to solve 24 TPTP problems not previously solved by any prover, including previous versions of Vampire .

Abstract The Vampire automated theorem prover is extended to output proofs in such a way that each inference is represented by a quantifier-free SMT instance. If every instance is unsatisfiable, the proof can be considered verified by an external SMT solver. This pragmatic form of proof checking places only a very light burden on the SMT solver, and can easily handle inferences that other systems may find difficult, such as theory inferences or extensive ground reasoning. The method is considerably easier to implement than proof formats based on small kernels and covers a greater variety of modern-day inferences.

Abstract During the past decade of continuous development, the theorem prover Vampire has become an automated solver for the combined theories of commonly-used data structures. Vampire now supports arithmetic, induction, and higher-order logic. These advances have been made to meet the demands of software verification, enabling Vampire to effectively complement SAT/SMT solvers and aid proof assistants. We explain how best to use Vampire in practice and review the main changes Vampire has undergone since its last tool presentation, focusing on the engineering principles and design choices we made during this process.

Abstract Program synthesis is the task of constructing a program conforming to a given specification. We focus on deductive synthesis, and in particular on synthesis problems with specifications given as $$\forall \exists $$ ∀ ∃ -formulas, expressing the existence of an output corresponding to any input. So far there has been no canonical benchmark set for deductive synthesis using the $$\forall \exists $$ ∀ ∃ -format and supporting the so-called uncomputable symbol restriction. This work presents such a data set, composed by complementing existing benchmarks by new ones. Our data set is dynamically growing and should motivate future developments in the theory and practice of automating synthesis.

Abstract Modern superposition inference systems aim at reducing the search space by introducing redundancy criteria on clauses and inferences. This paper focuses on reducing the number of superposition inferences with a single clause by blocking inferences into some terms, provided there were previously made inferences of a certain form performed with predecessors of this clause. Other calculi based on blocking inferences, for example basic superposition, rely on variable abstraction or equality constraints to express irreducibility of terms, resulting however in blocking inferences with all subterms of the respective terms. Here we introduce reducibility constraints in superposition to enable a more expressive blocking mechanism for inferences. We show that our calculus remains (refutationally) complete and present redundancy notions. Our implementation in the theorem prover Vampire demonstrates a considerable reduction in the size of the search space when using our new calculus.

Abstract We turn saturation-based theorem proving into an automated framework for recursive program synthesis. We introduce magic axioms as valid induction axioms and use them together with answer literals in saturation. We introduce new inference rules for induction in saturation and use answer literals to synthesize recursive functions from these proof steps. Our proof-of-concept implementation in the Vampire theorem prover constructs recursive functions over algebraic data types, while proving inductive properties over these types.

Abstract Proof by induction is commonplace in modern mathematics and computational logic. This paper overviews and discusses our recent results in turning saturation-based first-order theorem proving into a powerful framework for automating inductive reasoning. We formalize applications of induction as new inference rules of the saturation process, add instances of appropriate induction schemata to the search space, and use these rules and instances immediately upon their addition for the purpose of guiding induction. Our results show, for example, that many problems from formal verification and mathematical theories can now be solved completely automatically using a first-order theorem prover.

Abstract We present an automated reasoning framework for synthesizing recursion-free programs using saturation-based theorem proving. Given a functional specification encoded as a first-order logical formula, we use a first-order theorem prover to both establish validity of this formula and discover program fragments satisfying the specification. As a result, when deriving a proof of program correctness, we also synthesize a program that is correct with respect to the given specification. We describe properties of the calculus that a saturation-based prover capable of synthesis should employ, and extend the superposition calculus in a corresponding way. We implemented our work in the first-order prover Vampire, extending the successful applicability of first-order proving to program synthesis.

Abstract Automated reasoning is routinely used in the rigorous construction and analysis of complex systems. Among different theories, arithmetic stands out as one of the most frequently used and at the same time one of the most challenging in the presence of quantifiers and uninterpreted function symbols. First-order theorem provers perform very well on quantified problems due to the efficient superposition calculus, but support for arithmetic reasoning is limited to heuristic axioms. In this paper, we introduce the $$\textsc {Alasca}$$ A L A S C A calculus that lifts superposition reasoning to the linear arithmetic domain. We show that $$\textsc {Alasca}$$ A L A S C A is both sound and complete with respect to an axiomatisation of linear arithmetic. We implemented and evaluated $$\textsc {Alasca}$$ A L A S C A using the Vampire theorem prover, solving many more challenging problems compared to state-of-the-art reasoners.

Abstract Integers are ubiquitous in programming and therefore also in applications of program analysis and verification. Such applications often require some sort of inductive reasoning. In this paper we analyze the challenge of automating inductive reasoning with integers. We introduce inference rules for integer induction within the saturation framework of first-order theorem proving. We implemented these rules in the theorem prover Vampire and evaluated our work against other state-of-the-art theorem provers. Our results demonstrate the strength of our approach by solving new problems coming from program analysis and mathematical properties of integers.

Functional programs over inductively defined data types, such as lists, binary trees and naturals, can naturally be defined using recursive equations over recursive functions. In first-order logic, function definitions can be considered as universally quantified equalities. Verifying functional program properties therefore requires inductive reasoning with both theories and quantifiers. In this paper we propose new extensions and generalizations to automate induction with recursive functions in saturation-based first-order theorem proving, using the superposition calculus. Instead of using function definitions as first-order axioms, we introduced new simplification rules for treating function definitions as rewrite rules. We guide inductive reasoning and strengthen induction schema using recursively defined functions. Our experimental results show that handling recursive definitions in superposition reasoning significantly improves automated reasoning with induction.

Abstract Reasoning with quantifiers and theories is at the core of many applications in program analysis and verification. Whilst the problem is undecidable in general and hard in practice, we have been making large pragmatic steps forward. Our previous work proposed an instantiation rule for theory reasoning that produced pragmatically useful instances. Whilst this led to an increase in performance, it had its limitations as the rule produces ground instances which (i) can be overly specific, thus not useful in proof search, and (ii) contribute to the already problematic search space explosion as many new instances are introduced. This paper begins by introducing that specifically addresses these two concerns as it produces general solutions and it is a simplification rule, i.e. it replaces an existing clause by a ‘simpler’ one. Encouraged by initial success with this new rule, we performed an experiment to identify further common cases where the complex structure of theory terms blocked existing methods. This resulted in four further simplification rules for theory reasoning. The resulting extensions are implemented in the Vampire theorem prover and evaluated on SMT-LIB, showing that the new extensions result in a considerable increase in the number of problems solved, including 90 problems unsolved by state-of-the-art SMT solvers.

It is known that one can extract Craig interpolants from so-called local proofs. An interpolant extracted from such a proof is a boolean combination of formulas occurring in the proof. However, standard complete proof systems, such as superposition, for theories having the interpolation property are not necessarily complete for local proofs: there are formulas having 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 number of general results about interpolant extraction and complexity of extracted interpolants. In particular, we prove that the number of quantifier alternations in first-order interpolants of formulas without quantifier alternations is unbounded. This result has far-reaching consequences for using local proofs as a foundation for interpolating proof systems: any such proof system should deal with formulas of arbitrary quantifier complexity. To search for alternatives for interpolating proof systems, we consider several variations on interpolation and local proofs. Namely, we give an algorithm for building interpolants from resolution refutations in logic without equality and discuss additional constraints when this approach can be also used for logic with equality. We finally propose a new direction related to interpolation via local proofs in first-order theories.

The theory of finite term algebras provides a natural framework to describe the semantics of functional languages. The ability to efficiently reason about term algebras is essential to automate program analysis and verification for functional or imperative programs over inductively defined data types such as lists and trees. However, as the theory of finite term algebras is not finitely axiomatizable, reasoning about quantified properties over term algebras is challenging.

This paper presents new features recently implemented in the theorem prover Vampire, namely support for first-order logic with a first class boolean sort (FOOL) and polymorphic arrays. In addition to having a first class boolean sort, FOOL also contains if-then-else and let-in expressions. We argue that presented extensions facilitate reasoning-based program analysis, both by increasing the expressivity of first-order reasoners and by gains in efficiency.

The design and architecture of every very large Web service is unique, and EasyChair is not an exception. This talk overviews design features of EasyChair, which may be interesting for the software engineering community.

PDFX is a rule-based system designed to reconstruct the logical structure of scholarly articles in PDF form, regardless of their formatting style. The system's output is an XML document that describes the input article's logical structure in terms of title, sections, tables, references, etc. and also links it to geometrical typesetting markers in the original PDF, such as paragraph and column breaks. The key aspect of the presented approach is that the rule set used relies on relative parameters derived from font and layout specifics of each article, rather than on a template-matching paradigm. The system thus obviates the need for domain- or layout-specific tuning or prior training, exploiting only typographical conventions inherent in scientific literature. Evaluated against a significantly varied corpus of articles from nearly 2000 different journals, PDFX gives a 77.45 F1 measure for top-level heading identification and 74.03 for extracting individual bibliographic items. The service is freely available for use at http://pdfx.cs.man.ac.uk/.

Interpolation is an important technique in verification and static analysis of programs. In particular, interpolants extracted from proofs of various properties are used in invariant generation and bounded model checking. A number of recent papers studies interpolation in various theories and also extraction of smaller interpolants from proofs. In particular, there are several algorithms for extracting of interpolants from so-called local proofs. The main contribution of this paper is a technique of minimising interpolants based on transformations of what we call the "grey area" of local proofs. Another contribution is a technique of transforming, under certain common conditions, arbitrary proofs into local ones.

We propose a new method for equivalence checking of RTL and schematic descriptions of memories using translation into first-order logic. Our method is based on a powerful abstraction of memories and address decoders within them. We propose two ways of axiomatizing some of the bit-vector operations, decoders, and memories. The first axiomatization uses an algebra of operations on bit-vectors. The second axiomatization considers a bit-vector as a unary relation and memory as a relation of larger arity. For some designs, including real-life designs, the second axiomatization results in a first-order problem falling into a known decidable fragment of first-order logic and suitable for solving by modern first-order provers. Equivalence of real-life memories can be verified in seconds with our approach.

In this paper, we present UNIDOOR, a deductive objectoriented database system (DOOD). We demonstrate the distinctive features of UNIDOOR data model and its query language. We then show how essential object-oriented and database management features, that were missing from other DOOD implementations, are successfully supported in UNIDOOR. These features include a scalable persistent store with crash recovery, database integrity and transaction control facilities in a multi-user environment.

We show the NP-completeness of the existential theory of term algebras with the Knuth--Bendix order by giving a nondeterministic polynomial-time algorithm for solving Knuth--Bendix ordering constraints.

Orientability of systems of equalities is the following problem: given a system of equalities s/sub 1/ /spl sime/ t/sub 1/, . . . , s/sub n/ /spl sime/ t/sub n/, does there exist a simplification ordering > which orients the system, that is for every i /spl isin/ {1, ..., n}, either s/sub i/ > t/sub i/ or t/sub i/ > s/sub i/. This problem can be used in rewriting for finding a canonical rewrite system for a system of equalities and in theorem proving for adjusting simplification orderings during completion. We prove that (rather surprisingly) the problem can be solved in polynomial time when we restrict ourselves to the Knuth-Bendix orderings.

In software verification it is often required to prove statements about heterogeneous domains containing elements of various sorts, such as counters, stacks, lists, trees and queues. Any domain with counters, stacks, lists, and trees (but not queues) can be easily seen a special case of the term algebra, and hence a decision procedure for term algebras can be applied to decide the first-order theory of such a domain. We present a quantifier-elimination procedure for the first-order theory of term algebra extended with queues. The complete axiomatization and decidability of this theory can be immediately derived from the procedure.

We present a bottom-up decision procedure for propositional modal logic K based on the inverse method. The procedure is based on the “inverted” version of a sequent calculus. To restrict the search space, we prove a number of redundancy criteria for derivations in the sequent calculus. We introduce a new technique of proving redundancy criteria, based on the analysis of tableau-based derivations in K. Moreover, another new technique is based on so-called traces . A new search with a strong notion of subsumption. This technique is based on so-called traces . A new formalization of the inverse method in the form of a path calculus considerably simplifies all proofs as compared to the previously published presentations of the inverse method. Experimental results demonstrate that our method is competitive with many state-of-the-art implementations of K.

The authors show the decidability of the existential theory of term algebras with any Knuth-Bendix ordering. They achieve this by giving a procedure for solving Knuth-Bendix ordering constraints. As for complexity, NP-hardness of the set of satisfiable quantifier-free formulas can be shown in the same way as by R. Nieuwenhuis (1993). The algorithm presented does not give an NP upper bound; we point out parts of our algorithm that may cause nonpolynomial behavior.

In software verification, it is often required to prove statements about heterogeneous domains containing elements of various sorts, such as counters, stacks, lists, trees and queues. Any domain with counters, stacks, lists, and trees (but not queues) can be easily seen as a special case of the term algebra, and hence a decision procedure for term algebras can be applied to decide the first-order theory of such a domain. We present a quantifier-elimination procedure for the first-order theory of term algebras extended with queues. The complete axiomatization and decidability of this theory can be immediately derived from the procedure.

We present a bottom-up decision procedure for propositional modal logic K based on the inverse method. The procedure is based on the "inverted" version of a sequent calculus. To restrict the search space; we prove a number of redundancy criteria for derivations in the sequent calculus. We introduce a new technique of proving redundancy criteria, based on the analysis of tableau-based derivations in K. Moreover another new technique is used to prove completeness of proof-search with a strong notion of subsumption. This technique is based on so-called traces. A new formalization of the inverse method in the form of a path calculus considerably simplifies all proofs as compared to the previously published presentations of the inverse method. Experimental results reported elsewhere demonstrate that our method is competitive with many state-of-the-art implementations of K.

We extend the traditional query languages by primitives for handling lists and trees. Our main results characterize the expressive power and data complexity of the following extended languages: (1) relational algebra with lists and trees, (2) nonrecursive [email protected]@@@ with lists and trees, (3) nonrecursive Prolog with lists and trees, (4) first-order logic over lists and trees.

Abstract We prove that for a natural class of first-order formulas the validity problem is -complete.

We overview recent results related to Herbrand's theorem and tableau-like methods of automated deduction and prove some new results. Based on an analysis and discussion of these results, new research directions are suggested.

values should be treated.There are two major approaches.We investigate complexity of the SUCCESS problem for logic query languages with complex values: check whether a query defines a nonempty set.The SUCCESS problem for recursive query languages with complex values is undecidable, so WC study the complexity of nonrecursive queries.By complcx values we understand values such as trees, finite sets, and multlscts.Due to the well-known correspondence between relational query languages and datalog, our results can be considered as results about relational query languages with complex values.The paper gives a complete complexity classification of the SUCCESS problem for nonrecursive logic programs over trees depending on the underlying signature, presence of negation, and range restrictedness.We also prove several results about finite sets and multisets.

This paper surveys various complexity results on different forms of logic programming. The main focus is on decidable forms of logic programming, in particular propositional logic programming and datalog, but we also mention general logic programming with function symbols. Next to classical results on plain logic programming (pure Horn clause programs), more recent results on various important extensions of logic programming are surveyed. These include logic programming with different forms of negation, disjunctive logic programming, logic programming with equality, and constraint logic programming. The complexity of the unification problem is also addressed.

The notion of simultaneous rigid E-unification was introduced in 1987 in the area of automated theorem proving with equality in sequent-based methods, for example the connection method or the tableau method. Recently, simultaneous rigid E-unification was shown undecidable. Despite the importance of this notion, for example in theorem proving in intuitionistic logic, very little is known of its decidable fragments. We prove decidability results for fragments of monadic simultaneous rigid E-unification and show the connections between this notion and some algorithmic problems of logic and computer science.

We develop a constraint-based technique which allows one to prove decidability and complexity results for sequent calculi. Specifically, we study decidability problems for the prenex fragment of intuitionistic logic. We introduce an analogue of Skolemization for intuitionistic logic with equality, prove PSPACE-completeness of two fragments of intuitionistic logic with and without equality and some other results. In the proofs, we use a combination of techniques of constraint satisfaction, loop-free sequent systems of intuitionistic logic and properties of simultaneous rigid E-unification.