Abschlussarbeit

Abstract

This thesis is dedicated to the formalization and proving of the representation theorem for cumulative reasoning using the proof assistant Coq. The theorem represents one of the central theorems of nonmonotonic logic. Nonmonotonic reasoning enables the revision of conclusions when new information becomes available and considers exceptions, which is closer to human thinking than classical monotonic logic. A typical example is "birds fly", a rule that normally holds but can be over- ridden by more specific information such as "penguins do not fly". Cumulative reasoning traces back to the work of Kraus, Lehmann and Magidor from 1990, who developed System C with its five rules. A distinctive feature of machine-verified formalization with Coq is that it guarantees absolute precision and completeness, while handwritten proofs may contain errors or use implicit assumptions. We begin with the syntactic formalization of the System C rules and then proceed to the semantic modeling of cumulative models. We restrict ourselves to propositional logic in order to keep the complexity manageable and to focus on the essential aspects of the KLM-Theorem. The formalization and proofs provide a reusable foundation for non-monotonic reasoning and create a basis for extensions in knowledge representation.