8.2 Wrapping it up (Theorem Proving)

Driver Predicate and Code Summary for the code of this Chapter.

The file prop.pl contains a simple driver for theorem proving:

theorem(Formula) :-         
        naonly(Formula,ConvFormula),
        \+ tabl(false(ConvFormula),[],_).

Test it! theorem(walk(john) v (~walk(john))).

All Files

Here's a summary of the files that make up the implementation we've discussed: