Implementing Circumscription Using a Tableau Method.
Ilkka Niemelä · 1996
. A tableau calculus for first-order circumscriptive reasoning is developed. Parallel circumscription with fixed and varying predicates with respect to Herbrand models is treated. 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. 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 (subset) minimal (Herbrand) models and each counter-model is not generated more than once. Then the calculus is extended to handle parallel circumscription. The circumscriptive calculus is sound in the general case and complete when no function symbols are allowed. 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. 1 INTRODUCTION We study the automation of first-order circumscriptive...