A Theorem-Prover for a Decidable Subset of Default Logic

Book One

Volume

Proceedings of the AAAI Conference on Artificial Intelligence, 3

Knowledge Representation and Problem Solving

Non-monotonic logic is an attempt to take into account such notions as incomplete knowledge and theory evolution. However the decidable theorem-prover issue has been so far unexplored. We propose such a theorem-prover for default logic with a restriction on the first-order formulae it deals with. This theorem-prover is based on the generalisation of a resolution technique named saturation, which was initially designed to test the consistency of a set of first-order formulae. We have proved that our algorithm is complete and that it always terminates for the selected subset of first-order formulae.