Tableau-based characterization and theorem proving for default logic |
| |
Authors: | Vincent Risch Camilla B Schwind |
| |
Affiliation: | (1) Department of Computer Science, University of Western Ontario, Middlesex College, N6A 6B7 London, Ontario, Canada;(2) Faculté des Sciences de Luminy, Laboratoire d'Informatique de Marseille, CNRS, 16 Avenue de Luminy Case 901, 13288 Marseille Cedex 9, France |
| |
Abstract: | In this paper, we present a new method for computing extensions and for deriving formulae from a default theory. It is based on the semantic tableaux method and works for default theories with a finite set of defaults that are formulated over a decidable subset of first-order logic. We prove that all extensions (if any) of a default theory can be produced by constructing the semantic tableau ofone formula built from the general laws and the default consequences. This result allows us to describe an algorithm that provides extensions if there are any, and to decide if there are none. Moreover, the method gives a necessary and sufficient criterion for the existence of extensions of default theories with finitely many defaults provided they are formulated on a decidable subset of FOL.This work was completed while the author was at CNRS, Marseille. |
| |
Keywords: | nonmonotonic logic default logic tableaux |
本文献已被 SpringerLink 等数据库收录! |
|