Implementing Circumscription Using a Tableau Method

A tableau calculus for first-order circumscriptive reasoning is developed. The aim is to handle parallel circumscription with fixed and varying predicates with respect to Herbrand models. First a new clausal tableau calculus for first-order reasoning is developed where a hyper-type rule is combined with a restricted analytical cut rule. Then the calculus is extended to handle parallel circumscription. The calculus is sound in the general case and complete when no function symbols are allowed. A low space complexity is obtained by employing a groundedness property of minimal models that enables a one branch at a time approach to constructing tableaux for circumscriptive inference. The use of a cut rule offers the advantages that when deciding logical consequence the space of counter-models is searched with a preference to minimal models and each counter-model is not generated more than once. 1 Introduction We study the automation of first-order circumscriptive reasoning. Circumscriptio..