Sesión Lógica y Computabilidad (II)

Diciembre 15, 11:40 ~ 12:00

A Propositional Davis-Putnam Based Proof Calculus for Reasoning with Default Rules

Cassano, Valentin

Introduced by Reiter in his seminal 1980 article: `A Logic for Default Reasoning', Default Reasoning (DR), short for reasoning with default rules, occupies a place of preference in the logical theory of non-monotonic reasoning (NMR). Numerous studies address DR from the perspective of consequence relations that fail to satisfy the \emph{Principle of Monotonicity}. In comparison to these studies, the development of proof calculi for DR has received lesser attention. This development is fundamental for, in the conventional sense of the term, a proof calculus for DR provides a mechanization of its inferential aspects, aiding in their understanding. The latter is not minor, as the inferential aspects of DR are sometimes obscured by the intricacies of procedural or fix-point definitions. In this respect, proof calculi for DR form niche of research worth of exploration, and are an essential part of the logical theory of NMR. It is an interesting historical remark that the first proof calculus for DR, in the sense just mentioned, did not appear until 1996 in an article authored by Bonatti, many years after Reiter's seminal paper (even though other proof-theoretical approaches to DR had been presented). In this work, Bonatti presents an \emph{anti-sequent calculus} for a propositional credulous consequence relation for DR. Bonatti's work marks the beginning of the development of proof calculi for DR. We show how a propositional version of DR can be naturally integrated in the framework of Davis-Putnam proof calculi. We do this via the modification of the Davis-Putnam proof calculus for Classical Propositional Logic (CPL) to allow for the inclusion of reasoning with default rules. The result is a proof calculus for DR. Intuitively, the proof calculus considers a \emph{default consequence} to be a sentence that \emph{follows from} a \emph{premiss structure} (a set of sentences and a set of default rules). Default consequences are justified with respect to \emph{all extensions} of the premiss structure from which they follow. Extensions are analogous to those defined by {\L}ukaszewicz. Indeed, the calculus presents a mechanization of the \emph{follow from} relation. The calculus is simple and natural. It retains also the capability of the Davis-Putnam proof calculus of CPL of witnessing the non-existence of proofs and of providing concrete counterexamples. We prove the correctness of the calculus and exemplify its behavior by way of examples. The Davis-Putnam based proof calculus for DR that we present builds on, and borrows ideas from, an earlier work on a Tableaux based proof calculus for DR. These two calculi provide a mechanization of the same \emph{follows from} relation for DR. However, considering that the Davis-Putnam procedure is one the most efficient proving methods for CPL, it seems natural to combine a Davis-Putnam based proof calculus for CPL with DR to pave the road for an efficient implementation of a proof calculus for the latter. In addition, the close similarity of the Davis-Putnam and the tableau based proof calculi for DR opens the possibility for a formulation of a more abstract theory of expansion systems for DR. This may provide a unifying framework for the study of proof calculi for DR that is independent of the particular details of the calculi themselves.

Autores: Cassano, Valentin / Areces, Carlos.