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 two SZS answer formats, a short form suitable for a definite answers, and a long form which has greater expressive power. In both 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 Short Answer Form

The short form will be ...

    SZS answers short list_of_definite_answer_tuples_goes_here

... e.g., ...

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

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

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

The format of the tuples is not set in stone - I just want something trivial to parse and extract the terms.

The Long Answer Form

The long form will be ...

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

There can be mulitple 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 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 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 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 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 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 end for ANS001+1