Abstract

To give a standard against which to judge the limitations and possibilities of a theory of nonmonotonic reasoning, V. Lifschitz presented a paper at the 1988 Second International Workshop on Non-Monotonic Reasoning entitled "Benchmark Problems for Formal Nonmonotonic Reasoning." We show in this work the application of the modal logic Z to these benchmark problems. The modal logic Z provides a consistency-based approach to nonmonotonic reasoning. Z is a fragment of second order modal quantificational logic involving quantification over propositions but not over properties. We demonstrate that Z leads to correct and concise solutions to all the benchmark problems. We also show that many solutions to nonmonotonic reasoning problems expressed in Z are automatically derivable. Because we are able to solve the benchmark problems by hand using a small number of lemmas, we claim that Z has a learnable proof theory. ;In addition to handling all the benchmark problems, which to our knowledge has not been demonstrated for a single system of nonmonotonic reasoning, we also make a number of smaller contributions. This work provides solutions to the unique name problems which, to our knowledge, have not been solved by any other formal system. It demonstrates a new representation in Z for temporal projection, and improves on a representation by Lifschitz for temporal explanation. It describes a way of generalizing temporal projection to handle concurrent actions, and a way of using temporal explanation for counterfactual reasoning. It shows that Z is able to reason correctly about autoepistemic problems, including problems with quantification. Finally, it reports results on our use of and extensions to a theorem prover for Z