View: session overviewtalk overviewside by side with other conferences

09:00-10:30 Session 83P: Vampire - Past, Present and Future
Vampire: where have we come from, where are we going

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.

10:30-11:00Coffee Break
11:00-12:00 Session 86Q: Invited Talk
Counterexample-Guided Quantifier Instantiation in Logical Theories
12:30-14:00Lunch Break
14:00-15:30 Session 87Q: Contributed Talks
Towards Word Sense Disambiguation by Reasoning
SPEAKER: Javier Álvez

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.

Testing ATP folklore: a statistical analysis of Vampire proofs.

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.

Foundations of SPECTRE


15:30-16:00Coffee Break
16:00-17:30 Session 88L: Contributed Talks
Experimenting with Theory Instantiation in Vampire
SPEAKER: Martin Riener

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.

Giving AVATAR Quantifiers to Play With
SPEAKER: Martin Suda

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.

Developments in Higher-order Theorem proving within Vampire
SPEAKER: Ahmed Bhayat

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.

19:00-21:30 Workshops dinner at Keble College

Workshops dinner at Keble College. Drinks reception from 7pm, to be seated by 7:30 (pre-booking via FLoC registration system required; guests welcome).

Location: Keble College