Answer Extraction for TPTP

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.

Questions

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

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

Answers

• Answers may contain only variables, and symbols from the input formulae. That excludes, e.g., Skolem symbols.

• More general answers are preferred over less general. If all terms are answers, a variable should be output.

• For existentially quantified variables from interpreted domains, domain elements are preferred as answer values. Examples of interpreted domain are the numeric domains $int, $rat, $real, and "double quoted" distinct objects,
  • 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 existentially quantified variables from uninterpreted domains, constants are preferred as answer values. Examples of uninterpreted domains are $i in typed logics (e.g., THF and TFF), and the Herbrand Universe in untyped logics (e.g., FOF and CNF),

For returning answers, two SZS answer forms are proposed:

• The AnswerBindings form for returning answers in tuples
• The AnswerFormulae form for returning answers in the instantiated question

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(qq,axiom,! [U,V] : q(U,V) ).
    fof(xyz,question, ? [X,Y,Z] : ! [W] : ( p(X,Y,Z) & q(X,W) ) ).

The AnswerBindings Form

    SZS output start AnswerBindings
    answer bindings one per line
    SZS output end AnswerBindings

    % SZS status Success for ANS001+1
    % SZS output start AnswerBindings
    [bind(X,a),bind(Y,b),bind(Z,c)]
    [bind(X,d),bind(Y,e),bind(Z,f)]
    % SZS output end AnswerBindings

Disjunctive answers can also be expressed, e.g., ...

    % SZS status Success for ANS001+1
    % SZS output start AnswerBindings for ANS001+1
    [bind(X,g),bind(Y,h),bind(Z,i)] | [bind(X,j),bind(Y,k),bind(Z,l)]
    % SZS output end InstantiatedFormulae for ANS001+1

A final line with variables indicates that there might be more answers than the preceding tuples, e.g., ...

    % SZS status Success for ANS001+1
    % SZS output start AnswerBindings
    [bind(X,a),bind(Y,b),bind(Z,c)]
    [bind(X,d),bind(Y,e),bind(Z,f)]
    [bind(X,X),bind(Y,Y),bind(Z,Z)]
    % SZS output end AnswerBindings

The InstantiatedFormulae Answer Form

    % SZS answers start InstantiatedFormulae for ANS001+1
    instantiated annotated formulae
    % SZS answers end InstantiatedFormulae for ANS001+1

    % SZS status Success for ANS001+1
    % SZS output start InstantiatedFormulae for ANS001+1
    fof(xyz,answer, ! [W] : ( p(a,b,c) & q(a,W) ) ).
    fof(xyz,answer, ! [W] : ( p(d,e,f) & q(d,W) ) ).
    % SZS output end InstantiatedFormulae for ANS001+1

    % SZS status Success for ANS001+1
    % SZS output start InstantiatedFormulae for ANS001+1
    fof(xyz,answer, ! [W] : ( ( p(g,h,i) & q(g,W) ) | ( p(j,k,l) & q(j,W) ) ) ).
    % SZS output end InstantiatedFormulae for ANS001+1

A final line with existentially quantified variables indicates that there might be more answers than the preceding instantiated formulae, e.g., ...

    % SZS status Success for ANS001+1
    % SZS answers start InstantiatedFormulae for ANS001+1
    fof(xyz,answer, ! [W] : ( p(a,b,c) & q(a,W) ) ).
    fof(xyz,answer, ! [W] : ( p(d,e,f) & q(d,W) ) ).
    fof(xyz,answer, ? [X,Y,Z] : ! [W] : ( p(X,Y,Z) & q(X,W) ) ).
    % SZS answers end InstantiatedFormulae for ANS001+1

Additional Control

$unify

Axioms	Question	Answer
p(a), p(b), a = b	? [X] : ( p(X) & X != a )	No answer
p(a), p(b), a = b	? [X] : ( p(X) & ~$unify(X,a) )	[bind(X,b)]
! [X] : p(X)	? [X] : p(X)	No answer (Skolem's not permitted). This one is interesting - as a conjecture it's provable, but as a question it's not answerable. I like that!
! [Z] : p(Z)	? [X] : (p(X) & ? [Y] : $unify(X,f(Y)))	[bind(X,Z)]
p(f(a))	? [X] : (p(X) & ? [Y] : $unify(X,f(Y)))	[bind(X,f(a))]
! [Z] : p(Z)	? [X] : p(f(X))	[bind(X,Z1)]
p(f(a))	? [X] : p(f(X))	[bind(X,a)]
Aunt Agatha	? [X] : ( killed(X,agatha) & ( $unify(X,agatha) | $unify(X,butler) | $unify(X,charles) ) )	[bind(X,agatha)]
p(a) & p(b)	? [X] : ( p(X) & ~$unify(X,a))	[bind(X,b)]
Axioms for arrays, Swap array elements, array, indices i, j	? [X: $o] : (X => (array[i] != array[j])) Switch the contents of array[i] and array[j] such that the resultant array is different.	[bind(X,(i != j) & (array[i] != array[j])]
! [X] : mul(inv(X),X) = id ! [X] : mul(id,X) = X ! [X,Y,Z] : mul(X,mul(Y,Z)) = mul(mul(X,Y),Z)	? [X] : mul(e1,X) = id	[bind(X,inv(e1))]
! [X] : mul(inv(X),X) = id ! [X] : mul(id,X) = X ! [X,Y,Z] : mul(X,mul(Y,Z)) = mul(mul(X,Y),Z) ! [X] : mul(X,id) = X	? [Z] : ( (mul(e1,e2) = Y) => (mul(Z,Z) != id) )	[bind(Z, $ite(mul(e1,mul(e2,e1)) = e2, e1, $ite(id = mul(e2,mul(e1,e2))), e1, mul(e1,e2))))]

$contains

Axioms	Question	Answer
sunday | monday monday => workshop(vampire) sunday => workshop(arcade)	? [X]: workshop(X)	[bind(X,$ite(workshop(vampire),vampire,arcade))]
sunday | monday monday => workshop(vampire) sunday => workshop(arcade)	? [X]: ( workshop(X) & ~$contains(X,workshop) )	[bind(X,vampire)] | [bind(X,arcade)]
! [X] : mul(inv(X),X) = id ! [X] : mul(id,X) = X ! [X,Y,Z] : mul(X,mul(Y,Z)) = mul(mul(X,Y),Z)	? [X]: mul(X, mul(inv(a), inv(b))) != id	[bind(X,inv(mul(inv(a), inv(b)))]
! [X] : mul(inv(X),X) = id ! [X] : mul(id,X) = X ! [X,Y,Z] : mul(X,mul(Y,Z)) = mul(mul(X,Y),Z)	? [X]: ( mul(X, mul(inv(a), inv(b))) != id & ~contains(X,inv) )	[bind(X,TBA)]