Running Example

Question

p(a,b) p(a,f(b,c)) ∀Z p(b,Z) ∀Z p(Z,c) a != b a = c
Question: ∃X,Y p(X,Y)

Answers

Answers: X=a,Y=b; X=a,Y=f(b,c); X=b,Y=Z; X=c,Y=b; ... etc.

TPTP format Question

    fof(pab,axiom,      p(a,b)            ).
    fof(pafbc,axiom,    p(a,f(b,c))       ).
    fof(pbZ,axiom,      ! [Z] : p(b,Z)    ).
    fof(pZc,axiom,      ! [Z] : p(Z,c)    ).
    fof(a_not_b,axiom,  a != b            ).
    fof(a_is_c,axiom,   a = c             ).
    fof(pXY,question,   ? [X,Y] : p(X,Y)  ).

TPTP format Answers

SZS answers Tuple for ANS001+1 [[a,b],[b,Z],[a,c]]

SZS answers start Formulae for ANS001+1
fof(1,answer,
    ? [X,Y] :
      ( X = a & Y = b & p(X,Y) ),
    answer_to(pXY,[])).
fof(2,answer,
    ? [X,Y] :
      ( X = b & Y = Z & p(X,Y) ),
    answer_to(pXY,[])).
fof(3,answer,
    ? [X,Y] :
      ( X = a & Y = c & p(X,Y) ),
    answer_to(pXY,[])).
SZS answers end Formulae for ANS001+1

Denying Previous Answers with Inequalities

    fof(pXY,question,   ? [X,Y] : ( p(X,Y) ).                 p(a,b)
    %----Answer [a,b]                                         p(a,f(b,c))
                                                              ∀Z p(b,Z)
    fof(pXY,question,   ? [X,Y] : ( p(X,Y) &                  ∀Z p(Z,c)
        (X != a | Y != b) )  ).                               a != b
    %----Answer [b,Z]                                         a = c

    fof(pXY,question,   ? [X,Y] : ! [Z] : ( p(X,Y) & 
        (X != a | Y != b) & (X != b | Y != Z) )  ).
    %----Answer [a,c]

    fof(pXY,question,   ? [X,Y] : ! [Z] : ( p(X,Y) & 
        (X != a | Y != b) & (X != b | Y != Z) &
        (X != a | Y != c) )  ).
    %----CounterSatisfiable.

Answers: [[a,b],[b,Z],[a,c]] (modulo a = c)

Denying Previous Answers with "look different" Axioms

    fof(pXY,question,   ? [X,Y] : ( p(X,Y) ).                 p(a,b)
    %----Answer [a,b]                                         p(a,f(b,c))
                                                              ∀Z p(b,Z)
    fof(ld__a_b,axiom,  ld__(a,b)  ).                         ∀Z p(Z,c)
    fof(ld__a_c,axiom,  ld__(a,c)  ).                         a != b
    fof(ld__a_f,axiom,  ! [X,Y] : ld__(a,f(X,Y))  ).          a = c
    fof(ld__b_c,axiom,  ld__(b,c)  ).
    fof(ld__b_f,axiom,  ! [X,Y] : ld__(b,f(X,Y))  ).
    fof(ld__symmetry,axiom,! [X,Y] : (ld__(X,Y) => ld__(Y,X))  ).
    fof(pXY,question,   ? [X,Y] : ( p(X,Y) & 
        (ld__(X,a) | ld__(Y,b)) )  ).
    %----Answer [a,f(b,c)]

    fof(ld__c_f,axiom,  ! [X,Y] : ld__(c,f(X,Y))  ).
    fof(ld__f_f,axiom,  ! [X11,X12,X21,X22] :
        ( (ld__(X11,X12) | ld__(X21,X22))
       => ld__(f(X11,X21),f(X12,X22)) )  ).
    fof(pXY,question,   ? [X,Y] : ( p(X,Y) & 
        (ld__(X,a) | ld__(Y,b)) & 
        (ld__(X,a) | ld__(Y,f(b,c))) )  ).
    %----Answer [b,Z]

    etc.

Answers: [[a,b],[a,f(b,c)],[b,Z],[a,c],[c,c],[f(X,Y),c]]

Equality Testing

Unequal

    %----Answers [[a,b],[a,f(b,c)]], then [b,Z]
    fof(new,conjecture, ? [Z] :
        ( ( b != a | Z != b) & (b != a | Z != f(b,c)) )  ).
    %----Theorem

Answer [b,Z] is accepted.

Equal

    %----Answers [[a,b],[a,f(b,c)],[b,Z],[a,c]] 
    %----Answer [c,c]. Fail Unequal.
    fof(old,conjecture, ? [Z] :
        ( (c = a & c = b) | (c = a & c = f(b,c)) |
          (c = b & c = Z) | (c = a & c = c) )  ).
    %----Theorem.

Answer [c,c] is rejected.

Not Equal

    %----Answer [a,b]. Fail Unequal and Equal.
    fof(old,conjecture, (a = a & f(b,c) = b)  ).
    CounterSatisfiable

Answer [a,b] is accepted.

Not Unequal

    %----Answers [[a,b],[a,f(b,c)],[b,Z]] 
    %----Answer [c,c]. Fail (imagine) Unequal, Equal, Not equal
    fof(new,conjecture, ? [Z] :
        ( (a = a & c = b) | (a = a & c = f(b,c)) | 
          (a = b & c = Z) )  ).
    %----Theorem

Answer [c,c] is accepted.

Otherwise