@inproceedings{05f2d7c460024eb4995d5acdd6157b1e,
title = "The KLM Representation Theorem for System C, Formally",
abstract = "Wepresent a formalization of the proof of the correspondence between cumulative non-monotonic reasoning and System C in a proof assistant. Reasoning based on System C is the cornerstone of non-monotonic reasoning and was given a semantics via cumulative models by Kraus, Lehmann and Magidor. Our proof is inspired by the original proof and written in the proof system Rocq and focuses on propositional logic. Due to the features of Rocq, the proof implicitly yields a verified implementation of System C reasoning.",
author = "Jonathan Walther and Kai Sauerwald and Jesse Heyninck",
year = "2025",
language = "English",
volume = "4071",
series = "CEUR Workshop Proceedings",
publisher = "CEUR-WS.org",
pages = "281--294",
editor = "Anna Rapberger and Sebastian Rudolph",
booktitle = "Proceedings of the 23rd International Workshop on Non-Monotonic Reasoning (NMR 2025) co-located with the 22nd International Conference on Principles of Knowledge Representation and Reasoning (KR 2025), Melbourne, Australia, November 11-13, 2025",
address = "Germany",
}