Monotone Proofs in Predicate Default Logic with the Domain Closure Assumption

Robert Milnikel,

The addition of infinitary rules to the base logic of a default logic system can have a significant impact on the the complexity of monotone proofs in the system. In particular, proofs are no longer necessarily finite, but have depths bounded by recursive ordinals. It is suggested in [1] that open defaults in predicate default theories be dealt with via a domain closure assumption, instantiated as a rule of inference with infinitely many premises. We will examine the impact of such infinitary rules on proof schemes (as defined in [2]) and on tableau proof systems for skeptical consequence (as defined in [3]).

[1] M. Kaminski, J.A. Makowsky, and M. Tiomkin. Extensions for Open Default Theories via the Domain Closure Assumption. Journal of Logic and Computation, 8:169-187, 1998.

[2] W. Marek, A. Nerode, and J.B. Remmel. Nonmonotonic Rule Systems I. Annals of Mathematics and Artificial Intelligence, 1:241-273, 1990.

[3] R. Milnikel. Tableau Proof Systems for Skeptical Consequence. Proceedings, FLoC Workshop on Complexity-Theoretic and Recursion-Theoretic Methods in Databases, Artificial Intelligence, and Finite Model Theory, T. Eiter, G. Gottlob, V.W. Marek, and J.B. Remmel, eds.

Address: Wellesley College, 668 Washington St. #7, Wellesley, 2482, MA, USA

E-mail: rmilnikel@wellesley.edu