ABSTRACT. Over the past years Vampire has been progressively improving its ability to reason with quantifiers and theories. Originally theory reasoning was only via theory axioms and evaluation but over the past year two new techniques have been introduced. The first is the recent work of AVATAR modulo theories, previously presented, for ground theory reasoning. The second, the focus of this talk, consists of two new methods for reasoning with non-ground theory clauses (where we currently focus on the theory of arithmetic). The first new method is \emph{unification with abstraction} where the notion of unification is extended to introduce constraints where theory terms may not otherwise unify e.g. p(2) may unify with ~p(x+1) v q(x) to produce 2 != x+1 v q(x). This abstraction is performed lazily, as needed, to allow the superposition theorem prover to make as much progress as possible without the search space growing too quickly. The second new method utilises theory constraint solving (an SMT solver) to perform reasoning within a clause to find an instance where we can remove theory literals. This utilises the power of SMT solvers for theory reasoning with non-ground clauses, reasoning which is currently achieved by the addition of prolific theory axioms. Additionally, this second method can be used to discharge the constraints introduced by unification with abstraction. These methods were implemented within the Vampire theorem prover and experimental results show that they are useful for solving currently unsolved problems.

ABSTRACT. While interactive proof assistants for higher-order logic (HOL) commonly admit reasoning within rich type systems, current theorem provers for HOL are mainly based on simply typed Lambda-calculi and therefore do not allow such flexibility. In this paper, we present modifications to %the calculus and the implementation of the higher-order automated theorem prover Leo-III for turning it into a reasoning system for rank-1 polymorphic HOL. To that end, a polymorphic version of HOL and a suitable paramodulation-based calculus are sketched. The implementation is evaluated using a set of polymorphic TPTP problems encoded in the novel TH1 format.

ABSTRACT. Automated reasoning systems such as theorem provers often employ interaction or cooperation with further reasoning software. Whereas in most cases the concrete choice of cooperating software is, to some extent, irrelevant, these systems are nevertheless often fixed in practice due to compatibility issues. In order to support more flexible cooperation schemes, a machine-readable description format for automated reasoning systems' capabilities is proposed. Additionally, a simple HTTP-based protocol for system and capability discovery is outlined. Both the format and the protocol are designed to be simple, extensible and easy to use with none to minor modifications for existing reasoning systems.

ABSTRACT. In this paper we present an approach for reasoning with large theories which is based on the abstraction-refinement framework. The proposed approach consists of two approximations: the over-approximation, the under-approximation, and their combination.

ABSTRACT. This paper describes initial experiments using the set of support strategy to improve how a saturation-based theorem prover performs theory reasoning with explicit theory axioms. When dealing with theories such as arithmetic, modern automated theorem provers often resort to adding explicit theory axioms, for example x+y = y+x. Reasoning with such axioms can be explosive. However, little has been done to explore methods that mitigate the negative impact of theory axioms on saturation-based reasoning. The set of support strategy requires that all inferences involve a premise with an ancestor in a so-called set of support, initially taken to be a subset of the input clauses, usually those corresponding to the goal. This leads to completely goal orientated reasoning but is, in general, incomplete. The idea of this paper is to apply the set of support strategy to theory axioms only, and then to explore the effect of allowing some limited reasoning within this set. The suggested approach is implemented and evaluated within the Vampire theorem prover.