Answer Variables

Geoff Sutcliffe
University of Miami
geoff[@]cs.miami.edu

Some of these ideas come from emails with Pace Reagan Smith.

Introduction

There some users of the TPTP language, the people working towards common sense reasoning with ontologies, specifically the Cyc people and the SUMO person, who want to have reasoning systems return "answers" to "queries", e.g., "What is the capital of Afghanistan?" would return "Kabul". Simplistically one is tempted to express such queries using an exitentially quantified variable, and return the binding for the variable when a proof has been completed, e.g.,

fof(query,conjecture,
    ? [X] : capital(X,afghanistan) ).

However, this naive approach has problems:

If the answer is disjunction, e.g., given p(a) | p(b) and the query ? [X] : p(X). (In a proof by refutation the conjecture is used twice, with different bindings for X.)
The reasoning typically stops after one binding is found, while users my want multiple answers, e.g., "all rulers of Afghanistan", "two streets in Kabul", "at least seven tailors from Kabul", "no more than three countries that have a common border with Afghanistan", etc.

Additional to the need to return answers, the users want to be able to assert properties of the answers, which can be checked to ensure that the reasoning is correct. Examples are:

"we expect these results to be exactly the results found"
"we expect these results to be a subset of the results found"
"we expect these results to NOT be found"
"we expect exactly this number of results"
"we expect at least this number of results"
"we expect at most this number of results"
"we expect these results to NOT be found, or the system is unsound"
"we expect these results to be a subset of the results found, or the system is incomplete"
"we expect these results to be exactly the results found, or the system is either unsound or incomplete"

A TPTP Solution

However this is dealt with in the TPTP, it must be an extension of the core TPTP language. Rather, some TPTP meta-language seems appropriate, which can be used by a system to drive core ATP systems, and return answers. For example, given a request to find "two streets in Kabul", the meta-system could generate the conjecture

fof(query,conjecture,
    ? [S1,S2] : (street_in(kabul,S1) & street_in(kabul,S2) & S1 != S2) ).

then use an ATP system to generate a derivation, and extract the answers from the derivation.

However, it seems almost inevitable that in order to provide the full range of answer types efficiently, some cooperation from ATP systems is necessary. For example, to answer a query such as ""all rulers of Afghanistan", it would be possible by conjecturing

fof(query,conjecture,
    ? [R] : ruler(R,afghanistan) ).

and getting a first answer ahmad_shah_durrani, and then extending the conjecture to deny that answer

fof(query,conjecture,
    ? [R] : (ruler(R,afghanistan) & R != ahmad_shah_durrani) ).

and getting a second answer, etc, until the conjecture is found to be counter satisfiable. That would be posssible, but inefficient in various ways.

Maybe Defined Comments are the Answer

The TPTP language supports a convention of "defined comments":

%----Defined comments are a convention used for annotations that are used as
%----additional input for systems. They look like comments, but start with %$
%----or /*$. A wily user of the syntax can notice the $ and extract information
%----from the "comment" and pass that on as input to the system. They are
%----analogous to pragmas in programming languages. To extract these separately
%----from regular comments, the rules are:
%----      ::- |
%----     ::: [%]*
%----    ::: [/][*][*][*]*[/]
%----A string that matches both  and  should be
%----recognized as , so put these before .
%----Defined comments that are in use include:
%----    TO BE ANNOUNCED

These are being used already for notions of problem sets, problem series, and static properties of problem sets and series, e.g.,

%$ problem_set(cyc_series,[CSR025+1,CSR026+1,CSR027+1,CSR028+1,CSR029+1,CSR030+1,CSR031+1,CSR032+1,CSR033+1,CSR034+1,CSR035+1,CSR036+1])
%$ static(cyc_series,include('Axioms/CSR002+0.ax'))
include('Axioms/CSR002+0.ax').

Defined comments could be harnessed including meta-language statements in problems, which can be extracted by a meta-system, and also possibly used by an underlying ATP system. As the are comments, normal ATP system usage will ignore the these statements.