6.2 Wrapping it up (Theorem Proving)

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:

Further Reading

A textbook introduction to formal logics including a discussion of propositional and first-order tableaux methods is [Fit96].