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.

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)).

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

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

- 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.

SZS answers Tuple... e.g., ...list_of_definite_answer_tuples_goes_here

% SZS status Success for ANS001+1 % SZS answers Tuple [[a,b,c],[d,e,f]] for ANS001+1Disjunctive answers can also be expressed, e.g., ...

% SZS status Success for ANS001+1 % SZS answers Tuple [[a,b,c],[d,e,f],([g,h,i]|[j,k,l])] for ANS001+1To indicate that there are (or might be) more answers than those lists, the tuple can be terminated in a Prolog-like way with

% SZS answers Tuple [[a,b,c],[d,e,f]|_] for ANS001+1Lines 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

% SZS answers Instantiated... e.g., ...list_of_instantiated_formulae_goes_here

% SZS status Success for ANS001+1 % SZS answers Instantiated [p(a,b,c),p(d,e,f)] for ANS001+1Disjunctive answers can also be expressed, e.g., ...

% 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+1To indicate that there are (or might be) more answers than those lists, the tuple can be terminated in a Prolog-like way with

% SZS answers tuple for [p(a,b,c),p(d,e,f)|_] for ANS001+1Lines 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

% SZS answers start InstantiatedFormulae for ANS001+1There can be multiple fof encoded answers, each of which is an answer to the question. For example,fof_encoded_answers_go_here% SZS answers end InstantiatedFormulae for ANS001+1

% 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+1Disjunctive answers can also be expressed, e.g., ...

% 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

% SZS answers start Formulae for ANS001+1There 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_encoded_answers_go_here% SZS answers end Formulae for ANS001+1

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

% 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+1The []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

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