Lecturecise 20: Herbrand's Theorem and Resolution for First-Order Logic

Resolution Theorem Provers

Example of a very good theorem prover:

Our running example in latex:

(\forall x. \exists y.\ R(x,y)) \ \land \\
(\forall x.\forall y.\ (R(x,y) \rightarrow \forall z.\ R(x,f(y,z)))) \ \land \\
(\forall x.\ (P(x) \lor P(f(x,a)))) )\\
\rightarrow \forall x. \exists y.\ (R(x,y) \land P(y))

Input in TPTP3 format:

fof(axTotal,axiom,   ![X]:?[Y]: r(X,Y)).
fof(axExtends,axiom, ![X]:![Y]: (r(X,Y) => ![Z]:r(X,f(Y,Z)))).
fof(axAlt,axiom,     ![X]: (p(X) | p(f(X,a)))).
fof(c,conjecture,    ![X]:?[Y]: (r(X,Y) & p(Y))).

For Corresponding Output Click Here