ABSTRACT. In this session, I will give a broad overview of the Vampire system split into the past, present, and future. To begin with, I will give a quick beginner's guide to what Vampire is and what it looks like 'under the hood' focussing on new additions over the last 5 years. I will then talk about current projects and what you can expect to see in the near future. I will finish by talking about new ideas for the more distant future (i.e. things we haven't necessarily started working on yet). The session will be interactive and wherever possible I will show Vampire doing things.

ABSTRACT. In this proposal we describe a practical application of Vampire for Word Sense Disambiguation (WSD). In particular, we propose a method for the automatic disambiguation of the semantic relations in BLESS, which is a dataset designed to evaluate models of distributional semantics. It compiles 200 concrete nouns (100 animate and 100 inanimate nouns) from different classes and each noun is linked to other words via the semantic relations hyperonymy, cohyponymy, meronymy, attributes, events and random. For the disambiguation of the word pairs and semantic relations of BLESS, we have to map the words to WordNet synsets. WordNet is a large lexical database of English where nouns, verbs, adjectives and adverbs are grouped into sets of synonyms (synsets). Each synset denotes a distinct concept and they are interlinked among them by means of lexical-semantic relations such as synonymy, antonymy, hyponymy, meronymy or morphosemantic relations. Since a word can have different meanings, we need to choose which synset it belongs to, that is, the one that better fits the semantics of the word in the given context. To that end, we plan to use the knowledge in Adimen-SUMO, which is obtained by means of a suitable transformation of the knowledge in the core of SUMO into first-order logic (FOL) and enables its use by FOL automated theorem provers such as Vampire. WordNet and SUMO (and therefore Adimen-SUMO) are connected in a semantic mapping by means of three semantic relations: equivalence, subsumption and instance. By exploiting this mapping, we will automatically create a set of conjectures for each word pair by considering the semantic relations provided by BLESS. Then, these conjectures will be evaluated using Vampire. According to the outcomes, each word will be connected to a single synset and, consequently, disambiguated. Finally, we plan to compare the results provided by our proposal and different disambiguation systems that can be found in the literature.

ABSTRACT. There are a number of well-known assumptions about automated theorem proving such as "proofs usually only use a small proportion of the given axioms to prove a goal". In this talk we present a statistical analysis of a large number of Vampire proofs and use this to investigate a number of these assumptions coming from ATP folklore.

ABSTRACT. ~

ABSTRACT. Theory instantiation tackles the problem of theory reasoning with quantifiers in Vampire using an SMT solver. In contrast to AVATAR modulo theories it works locally by instantiating a clause such that its pure theory part becomes inconsistent and can be deleted. We present our experiments with different clause filtering strategies. This achieves two goals, better interaction with unification with abstraction as well as restricting the problem passed to the SMT solver to well supported theories like linear integer arithmetic.

ABSTRACT. We investigate an extension of the AVATAR architecture which exposes first-order variables to the underlying SMT-solver. This enables (a controlled amount of) quantifier instantiation effort from within the SMT solver to complement the first-order prover's native support for quantifier reasoning. We report on experimental results with Vampire combined with the SMT solver CVC4.

ABSTRACT. This talk presents on-going work on extending Vampire to higher-order reasoning. Currently, two strategies are being explored. A translation from higher to first-order logic has been implemented and a mixture of heuristics and special inference rules have been implemented to control the search procedure. Alternatively, we are working on extending Vampire's data structures to support higher-order features and then pragmatically introducing higher-order reasoning.