ABSTRACT. Reasoning about first-order quantified formulas in Satisfiablity Modulo Theories (SMT) solvers is a long standing challenge in the community. The most widely used technique in current SMT solvers for reasoning about quantified formulas is quantifier instantiation. This talk will survey advances in recent instantiation-based techniques, including refinements to the widely-used technique known as E-matching, as well as counterexample-guided approaches that are specialized to theories such as a linear real and integer arithmetic. We will focus on the practical aspects and implementation of these techniques in the SMT solver CVC4.

ABSTRACT. We describe new extensions of Vampire for supporting reasoning and proving properties of loops with arrays. The common theme of our work is the symbol elimination method for generating loop invariants. We first discuss a small change in the program analysis framework of Vampire which allows us to generate program properties with alternation of quantifiers, by simplifying skolemization during consequence finding. We then use the theory of polymorphic arrays to generate and prove program properties over arrays. We illustrate our approach on a number of examples coming from program verification.

ABSTRACT. Developing provably sound type systems is a non-trivial task which, as of today, typically requires expert skills in formal methods and a considerable amount of time. Our Veritas project aims at providing support for the development of soundness proofs of type systems and efficient type checker implementations from type system specifications. To this end, we investigate how to best automate typical steps within type soundness proofs. In this paper, we focus on progress proofs for type systems of domain-specific languages. As a running example for such a type system, we model a subset SQL and augment it with a type system. We compare two different approaches for automating proof steps of the progress proofs for this type system against each other: firstly, our own tool Veritas, which translates proof goals and specifications automatically to TPTP and calls Vampire on them, and secondly, the programming language Dafny, which translates proof goals and specifications to the intermediate verification language Boogie 2 and calls the SMT solver Z3 on them. We find that Vampire and Dafny are equally well-suited for automatically proving simple steps within progress proofs.

ABSTRACT. We report on the results of evaluating the performance automated theorem provers using Adimen-SUMO. The evaluation follows the adaptation of the methodology based on competency questions [6] to the framework of first-order logic, which is presented in [3], and is applied to Adimen-SUMO [1]. The set of competency questions used for this evaluation has been semi-automatically generated from a small set of semantic patterns and the mapping of WordNet to SUMO, also introduced in [3]. Our experimental results demonstrate that improved versions of the proposed set of competency questions could be really valuable for the development of automated theorem provers.

References: [1] J. Álvez, P. Lucio, and G. Rigau. Adimen-SUMO: Reengineering an ontology for first-order reasoning. Int. J. Semantic Web Inf. Syst., 8(4):80–116, 2012. [3] J. Álvez, P. Lucio, and G. Rigau. Improving the competency of first-order ontologies. In J. M. Gómez-Pérez, editor, Proc. of the 8th Int. Conf. on Knowledge Capture (K-CAP 2015). ACM, 2015. [6] M. Grüninger and M. S. Fox. Methodology for the design and evaluation of ontologies. In Proc. of the Workshop on Basic Ontological Issues in Knowledge Sharing (IJCAI 1995), 1995.

ABSTRACT. The theory of finite term algebras has long been a subject of interest for computer scientists. Such algebras can be used to formalize many mathematical objects, including the semantics of programming languages. Terms may even be the object of computation themselves, as illustrated by functional programming languages. The decidability of the full first-order fragment of this theory was established more than sixty years ago, however it is also known that it cannot be axiomatized by a finite set of sentences. Theory reasoning is therefore typically accomplished by using a dedicated decision procedure. This prevents us from using the full power of a general first-order theorem prover: in particular a decision procedure cannot reason in the presence of multiple theories. We present two ways to perform complete reasoning in the theory of finite term algebras in a saturation-based first-order theorem prover. The first is a conservative extension of the theory, which requires only a finite number of statements. This solution may be used in any existing theorem prover, but will not lead to optimal performance. We also consider another approach, namely extending the superposition calculus with additional inference rules to conduct theory reasoning. We evaluate both techniques on a number of known problems and compare the results to other automated reasoning systems.

ABSTRACT. FOOL is a modification of many-sorted first-order logic extended by syntactical constructs such as if-then-else, let-in, tuple expressions and tuple let-in expressions. These constructs can be used to straightforwardly encode properties of programs as formulas in FOOL. In this talk we show how next-state relations of loopless imperative programs can be efficiently expressed in FOOL, and then reasoned about with Vampire.

ABSTRACT. Global Subsumption is a simplification technique for saturation-based first-order theorem provers. The general idea is that we can replace a clause C by its subclause D if D follows from the initial problem as D will subsume C. The effectiveness of the technique comes from an effective approach for (incompletely) checking whether D is a consequence of the initial problem. Here the idea is to produce and maintain a set S of ground clauses that follow from the input (e.g. grounded versions of all derived clauses) and to check whether a grounding of D follows from this set. As this is now a propositional problem this check can be performed by a SAT solver, making it efficient. In this paper we review the global subsumption technique and consider various extensions and their implementations in the Vampire theorem prover. We consider, for example, which groundings to place in S, how to select the subclause(s) D to check, how to integrate this technique with the AVATAR approach and whether it makes sense to replace the SAT solver with a SMT solver.

ABSTRACT. A wide number of effective clause-elimination procedures for SAT is based on the clause-redundancy property called blocked clauses. In this paper, we introduce a generalization of blocked clauses to first-order logic and show how they can be used in a preprocessing step within an automated theorem prover. We report on experimental results obtained from a prototype implementation in Vampire.

ABSTRACT. Vampire produces highly usable and informative proofs, but now they are even better and this paper explains why. It is important that the proofs produced by automated theorem provers are both understandable and machine checkable. Producing something that satisfies both of these goals is challenging, especially when dealing with complex steps performed by the solver. The main areas where proof output has been improved for understanding include (i) introduction of new symbols (such as Skolem functions) in preprocessing, (ii) representation of unifiers (for example, in resolution steps), and (iii) presentation of AVATAR proofs. These improvements will be illustrated via a number of examples. For checkable proofs Vampire provides a mode that outputs the proof into a number of individual (TPTP) problems that can be independently proved. This process is explained and illustrated with examples.