Answer Extraction for TPTP

by Geoff Sutcliffe, Mark Stickel, Stephan Schulz, Josef Urban

Answer extraction is useful (and meaningful only) when there are existential quantifiers at the outermost level of a conjecture. In this situation the conjecture can be considered to a question for which an answer is required, in the form of the values that instantiate the existentially quantified variables. This proposal describes how such instantiations can be returned in a standard and useful way.

The new question role is introduced to identify conjectures for which the bindings for the outermost existentially quantified variables are wanted. For returning answers, four SZS answer forms are proposed:

The Tuple form for returning answers in a tuple
The Instantiated form for returning answers in the existentially quantified formula
The InstantiatedFormulae form for returning answers in the instantiated annotated formula
The Formulae form that has greater expressive power.

In all forms the answer output lines must be preceded by an SZS status line.

The following problem, from the problem file ANS001+1, is used as the running example ...

    fof(abc,axiom,p(a,b,c)).
    fof(def,axiom,p(d,e,f)).
    fof(ghi_or_jkl,axiom,( p(g,h,i) | p(j,k,l) )).
    fof(xyz,question, ? [X,Y,Z] : p(X,Y,Z)).

The Question Form

Questions are written like conjectures, but using the question role instead of the conjecture role. The outermost existentially quantified variables are the ones that the user wants values for, i.e., their sets of instatiations are the answer.

Trick: If the user wants values for only a subset of the outermost existentially quantified variables, a dummy universal quantification can be inserted, e.g., if the question is ...

    fof(xyz,question, ? [X,Y,Z] : p(X,Y,Z)).

... and the user wants values for only X and Z, it can be written as ...

    fof(xyz,question, ? [X,Z] : ! [D] : ? [Y] : p(X,Y,Z)).

Answers

Answers are bindings for the outermost existentially quantified variables.

For variables from interpreted domains, answers must be domain elements if possible. Examples of interpreted domain are the numeric domains $int, $rat, $real, and "double quoted" distinct objects,
- A consequence of that requirement is that ground interpreted terms, e.g., ground arithmetic terms, must be evaluated to domain elements.
- For ground terms that include underspecified functions, e.g., $to_rat and $quotient, it is not always "possible" to evaluate to a domain element.
For variables from uninterpreted domains, constants are preferred over non-constants for answers. Examples of uninterpreted domains are $i in typed logic forms (e.g., THF and TFF), and the Herbrand Universe in untyped logic forms (e.g., FOF and CNF),
If all terms are answers, a variable should be output. In this case the SZS result should differentiate between the cases of non-contradictory and contradictory axioms, e.g., by using the status values SatisfiableTheorem (STM) and ContradictoryAxioms (CAX) respectively.

The Tuple Answer Form

The tuple form is ...

    SZS answers Tuple list_of_definite_answer_tuples_goes_here

... e.g., ...

    % SZS status Success for ANS001+1
    % SZS answers Tuple [[a,b,c],[d,e,f]] for ANS001+1

Disjunctive answers can also be expressed, e.g., ... Should this be allowed?

    % SZS status Success for ANS001+1
    % SZS answers Tuple [[a,b,c],[d,e,f],([g,h,i]|[j,k,l])] for ANS001+1

To indicate that there are (or might be) more answers than those lists, the tuple can be terminated in a Prolog-like way with |_, e.g., ...

    % SZS answers Tuple [[a,b,c],[d,e,f]|_] for ANS001+1

Lines may have a : to indicate the start of system/task specific information. For example:

    % SZS answers Tuple [[a,b,c],[d,e,f]] for ANS001+1 : Used OASys

The Instantiated Answer Form

It is expected that in many applications the answers returned will be used as logical data in a subsequent reasoning process. In that case it's convenient to have the data in a logical form, rather than a tuple. The instantiated form provides an atomic logical form ...

    % SZS answers Instantiated list_of_instantiated_formulae_goes_here

... e.g., ...

    % SZS status Success for ANS001+1
    % SZS answers Instantiated [p(a,b,c),p(d,e,f)] for ANS001+1

Disjunctive answers can also be expressed, e.g., ... Should this be allowed?

    % SZS status Success for ANS001+1
    % SZS answers Instantiated [p(a,b,c),p(d,e,f),(p(g,h,i) | p(j,k,l)] for ANS001+1

To indicate that there are (or might be) more answers than those lists, the tuple can be terminated in a Prolog-like way with |_, e.g., ...

    % SZS answers tuple for [p(a,b,c),p(d,e,f)|_] for ANS001+1

Lines may have a : to indicate the start of system/task specific information. For example:

    % SZS answers Instantiated [p(a,b,c),p(d,e,f)] for ANS001+1 : Used OASys

The InstantiatedFormulae Answer Form

The instantiated formulae form provides answers in the TPTP FOF format, so that all TPTP tools can work with the answers, and the answers can be used directly, e.g., as axioms, in subsequent reasoning processes. The instantiated formulae form is ...

    % SZS answers start InstantiatedFormulae for ANS001+1
    fof_encoded_answers_go_here
    % SZS answers end InstantiatedFormulae for ANS001+1

There can be multiple fof encoded answers, each of which is an answer to the question. For example,

    % SZS status Success for ANS001+1
    % SZS answers start InstantiatedFormulae for ANS001+1
    fof(1,answer,
        p(a,b,c),
        answer_to(xyz,[])).
    fof(2,answer,
        p(d,e,f),
        answer_to(xyz,[])).
    % SZS answers end InstantiatedFormulae for ANS001+1

Disjunctive answers can also be expressed, e.g., ... Should this be allowed?

    % SZS status Success for ANS001+1
    % SZS answers start InstantiatedFormulae for ANS001+1
    fof(3,answer,
        ( p(g,h,i) 
        | p(j,k,l) ),
        answer_to(xyz,[])).
    % SZS answers end InstantiatedFormulae for ANS001+1

The Formulae Form

The formulae form is ...

    % SZS answers start Formulae for ANS001+1
    fof_encoded_answers_go_here
    % SZS answers end Formulae for ANS001+1

There can be multiple fof encoded answers, each of which is an answer to the question. The fullest form of a fof encoded answer is ...

    fof(some_name,answer,
        quantification_from_question
            disjunction_of_conjunctions_of_binding_equations & the_question,
        answer_to(name_of_question,[])).

... e.g., ...

    % SZS status Success for ANS001+1
    % SZS answers start Formulae for ANS001+1
    fof(1,answer,
        ? [X,Y,Z] :
          ( X = a & Y = b & Z = c & p(X,Y,Z) ),
        answer_to(xyz,[])).
    fof(2,answer,
        ? [X,Y,Z] :
          ( X = d & Y = e & Z = f & p(X,Y,Z) ),
        answer_to(xyz,[])).
    fof(3,answer,
        ? [X,Y,Z] :
          ( ( ( X = g & Y = h & Z = i )
            | ( X = j & Y = k & Z = l ) )
          & p(X,Y,Z) ),
        answer_to(xyz,[])).
    % SZS answers end Formulae for ANS001+1

The []s in the answer_to term are for useful_info, in the TPTP syntax tradition.

It is possible that this long form asks too much of some systems, so it is tolerable to omit either the_question or the answer_to term, or both. Additionally, the answer variables may be renamed (but not reordered). For example, a minimal long form would be ...

    % SZS status Success for ANS001+1
    % SZS answers start Formulae for ANS001+1
    fof(1,answer, ? [U,V,W] : ( U = a & V = b & W = c )).
    fof(2,answer, ? [K,J,L] : ( K = d & J = e & L = f )).
    fof(3,answer, ? [Z,Y,X] : ( ( Z = g & Y = h & X = i )
                              | ( Z = j & Y = k & X = l ) )).
    % SZS answers end Formulae for ANS001+1

Multiple Questions

A TPTP problem file can have multiple conjectures, and the problem is solved when all conjectures have been proved. Similarly a TPTP problem file can have multiple questions, and the problem is solved when all questions have been answered. The answer_to provides differentiation between answers to different questions in the same problem file. For example, for the following problem from the problem file ANS002+1 ...

    fof(a,axiom,p(a)).
    fof(b,axiom,q(b)).
    fof(p,question,? [X] : p(X)).
    fof(q,question,? [X] : q(X)).

... the answer could be ...

    % SZS status Success for ANS002+1
    % SZS answers formulae start for ANS001+1
    fof(1,answer,? [X] : X = a & p(X),answer_to(p,[])).
    fof(2,answer,? [X] : X = b & q(X),answer_to(q,[])).
    % SZS answers formulae end for ANS001+1