10.2 Implementing First-Order Tableaux

As you'll probably expect from reading the theoretical section on first-order tableaux, the implementation of the new quantifier rules demands special care. Due to the undecidability of first-order logic, we cannot expect that we are done by translating the rules to Prolog and letting the program run. In fact, we not only have to add the two new quantifier clauses to our tableaux predicate tab/6 (formerly tabl/3). As you will see in a minute, we also have to replace our former base clause by four clauses controlling the instantiations of the universial quantifer. Last not least, we have to include a mechanism that ensures that our program really halts on every input. But let's approach the matter systematically.



Aljoscha Burchardt, Stephan Walter, Alexander Koller, Michael Kohlhase, Patrick Blackburn and Johan Bos
Version 1.2.5 (20030212)