Multiple Answer Extraction
for Question Answering with
Automated Theorem Proving Systems
Abstract
The Multiple ANSwer EXtraction system is a framework for
interpreting a conjecture with outermost existentially quantified variables
as a question, and extracting multiple answers to the question by repetitive
calls to a base system that can report the bindings for the variables in
one proof of the conjecture.
This paper describes the framework and demonstrates its use on an illustrative
example.