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 the conjecture of a FOF problem. In this situation the conjecture caqn 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 described how such instantiations can be returned in a standard and useful way.

There will be several SZS answer formats, a tuple form suitable for definite answers, a instantiated form for returning answers in the existentially quantified formula, and a 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 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 for ANS001+1 [[a,b,c],[d,e,f]]
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 ANS001+1 [[a,b,c],[d,e,f]|_]
Lines may have a : to indicate the start of system/task specific information. For example: 
    SZS answers tuple for ANS001+1 [[a,b,c],[d,e,f]] : Used OASys

The Instantiated Answer Form

The instantiated form is ... 
    SZS answers instantiated list_of_instantiated_formulae_goes_here
... e.g., ... 
    SZS status Success for ANS001+1
    SZS answers instantiated for ANS001+1 [p(a,b,c),p(d,e,f)]
Disjunctive answers can also be expressed, e.g., ... Should this be allowed? 
    SZS status Success for ANS001+1
    SZS answers instantiated for ANS001+1 [p(a,b,c),p(d,e,f),p(g,h,i) | p(j,k,l)]
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 ANS001+1 [[a,b,c],[d,e,f]|_]
Lines may have a : to indicate the start of system/task specific information. For example: 
    SZS answers instantiated for ANS001+1 [p(a,b,c),p(d,e,f)] : Used OASys

The Formulae Answer Form

The formulae form is ... 
    SZS answers formulae start for ANS001+1
    fof_encoded_answers_go_here
    SZS answers formulae end 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 formulae start 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 formulae end 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 formulae start 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 formulae end 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