Sequent-type calculi for variants of default logic

Abstract

Sequenzenkalküle sind eine wichtige Beweismethode in der automatischen Deduktion. In dieser Arbeit führen wir solche Kalküle für zwei Versionen von Default Logik ein, nämlich einerseits für eine dreiwertige Form der Default Logik, eingeführt von Radzikowska, und der Disjunktiven Default Logik nach Gelfond, Lifschitz, Przymusinska und Truszczyński. Die erste Variante von Default Logik verwendet die bekannte dreiwertige Logik von Łukasiewicz als zugrundeliegenden logischen Apparat, während in der Disjunktiven Default Logik verallgemeinerte Default Regeln verwendet werden, die eine Auswahl von Konklusionen erlauben. Beide Kalküle wurden eingeführt um gewisse Probleme der üblichen Default Logik zu adressieren. Die Kalküle die wir beschreiben axiomatisieren das sogenannte Brave Reasoningund folgen der Methode von Bonatti, der solche Kalküle im Bereich des Nichtmonotonen Schließens postulierte. Ein besonderes Merkmal der Kalküle von Bonatti ist die Verwendung eines komplementären Kalküls der Ungültigkeit formalisiert und der für die Axiomatisierung der Konsistenzbedingungen von Defaults zuständig ist.

Sequent-type proof systems constitute an important and widely used class of calculi well-suited for analyzing proof search. In this thesis, we introduce sequential-type calculi for two variants of default logic, namely, on the one hand, for disjunctive default logic, due to Gelfond et al., And, on the other hand, for three-valued default logic, due to Radzikowska. Lukasiewicz's well-known three-valued logic as the underlying base logic. In particular, our calculus axiomatises brave reasoning for these versions of default logic, following the sequential method first introduced in the context of nonmonotonic reasoning by Bonatti, which employs a complementary calculus for axiomatising invalid formulas, taking care of expressing the consistency condition of defaults.