LARA

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

PDF Slides

Resolution Theorem Provers

Example of a very good theorem prover:

Our running example in latex:

\begin{equation*} (\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)) \end{equation*}

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

More

Ground Terms

Herbrand Model for an Example

Herbrand's Expansion Theorem

Semidecision Procedure for First-Order Logic (without Equality)

Instantiation plus Ground Resolution

Non-Ground Instantiation and Resolution

Unification

Definition of Resolution for FOL

Completeness of Resolution for FOL