Answer Extraction for TPTP

by Geoff Sutcliffe, Michael Rawson, Petra Hozzova, Mark Stickel, Stephan Schulz,

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

The new question role is introduced to identify conjectures for which the bindings for the outermost existentially quantified variables are wanted. 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, e.g., ...

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

... and if the user wants values for only X and Z ...

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

In THF there can be universally quantified variables outside the existentially quantified variables, e.g., ...

    thf(lambda,question, ! [A: $int,B: $int] : ? [R: $int] : ( ($difference @ A @ R) = B ) ).

... in which case the answer is a lambda term.

Answers

Answers are bindings for the outermost existentially quantified variables.

Answers may contain only variables, and symbols from the input formulae. That excludes, e.g., Skolem symbols. This means that there is no answer to ...
```
     fof(some_p,axiom,? [X] : p(X) ).
     fof(is_there_some_p,questions,? [X] : p(X) ).
```
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),

The answer output lines are in the same style as SZS status and output lines.

The `answers` Tuple Form

The answers are give as a tuple of alternative answer tuples. For example:

fof(abc,axiom,p(a,b,c).
fof(def,axiom,p(d,e,f).
fof(xyz,question,? [X,Y,Z] : p(X,Y,Z) ).

One answer:

% SZS answers Tuple [[bind(X,a),bind(Y,b),bind(Z,c)]]

All answers

% SZS answers Tuple [[bind(X,a),bind(Y,b),bind(Z,c)],[bind(X,d),bind(Y,e),bind(Z,f)]]

Examples:

Axioms Question Answer

p(a,b,c)
p(d,e,f) ? [X,Y,Z] : p(X,Y,Z) [[bind(X,a),bind(Y,b),bind(Z,c)]] One answer
[[bind(X,a),bind(Y,b),bind(Z,c)],[bind(X,d),bind(Y,e),bind(Z,f)]] All answers

p(a)
p(b)
a = b ? [X] : ( p(X) & X != a ) No answer (but compare with ? [X] : ( p(X) & ~$unify(X,a) ) below)

! [X] : p(X) ? [Y] : p(Y) [[bind(Y,X)]]

? [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(f(X)) [bind(X,Z1)]

p(f(a)) ? [X] : p(f(X)) [bind(X,a)]

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

! [A: $int,B: $int] : ? [R: $int] : ( ($difference @ A @ R) = B )

[^ [A: $int,B: $int] : bind(R,$uminus($sum($uminus(A),B)))]

Axioms	Question	Answer

`p(a,b,c)` `p(d,e,f)`	`? [X,Y,Z] : p(X,Y,Z)`	`[[bind(X,a),bind(Y,b),bind(Z,c)]]` One answer `[[bind(X,a),bind(Y,b),bind(Z,c)],[bind(X,d),bind(Y,e),bind(Z,f)]]` All answers

`p(a)` `p(b)` `a = b`	`? [X] : ( p(X) & X != a )`	No answer (but compare with `? [X] : ( p(X) & ~$unify(X,a) )` below)

`! [X] : p(X)`	`? [Y] : p(Y)`	`[[bind(Y,X)]]`

`? [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(f(X))`	`[bind(X,Z1)]`

`p(f(a))`	`? [X] : p(f(X))`	`[bind(X,a)]`

`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))))]

	! [A: $int,B: $int] : ? [R: $int] : ( ($difference @ A @ R) = B )	[^ [A: $int,B: $int] : bind(R,$uminus($sum($uminus(A),B)))]

Additional Control

`$unify`

What we seem to need is $unify/2 that checks if two formulae can unify (but does not do the unification). It would be quite simple to implement.

Examples:

Axioms Question Answer

p(a)
p(b)
p(c) ? [X] : ( p(X) & ( $unify(X,a) | $unify(X,d) ) ) [bind(X,a)]

p(a)
p(b)
a = b ? [X] : ( p(X) & ~$unify(X,a) ) [bind(X,b)]

! [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))]

Axioms	Question	Answer

`p(a)` `p(b)` `p(c)`	`? [X] : ( p(X) & ( $unify(X,a) \| $unify(X,d) ) )`	`[bind(X,a)]`

`p(a)` `p(b)` `a = b`	`? [X] : ( p(X) & ~$unify(X,a) )`	`[bind(X,b)]`

`! [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))]`

`$contains`

Petra would also like $contains/2 that tests if a certain symbol occurs in an expression. It would be quite simple to implement.

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

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)]`