Open AccessRevisiting Question Answering in Vampire
Author(s) -
Giles Reger
Publication year - 2018
Publication title -
epic series in computing
Language(s) - English
Resource type - Conference proceedings
ISSN - 2398-7340
DOI - 10.29007/fjc4
Subject(s) - vampire , axiom , question answering , conjecture , automated theorem proving , computer science , process (computing) , variable (mathematics) , mathematics , theoretical computer science , discrete mathematics , artificial intelligence , programming language , mathematical analysis , geometry
Question answering is the process of taking a conjecture existentially quantified at the outer- most level and providing one or more instantiations of the quantified variable(s) as a form of an answer to the implied question. For example, given the axioms p(a) and f(a)=a the question ?[X] : p(f(X)) could return the answer X=a. This paper reviews the question answering prob- lem focussing on how it is tackled within the VAMPIRE theorem prover. It covers how VAMPIRE extracts single answers, multiple answers, disjunctive answers, and answers involving theories such as arithmetic. The paper finishes by considering possible future directions, such as integration with finite model finding.