Dear all,
Jonathan Walther
will deliver the next Oberseminar (20th February,10:00, via Zoom):
Title: “About Formalization and Semi-Automated Proof
of the Standard Representation Theorem for Cumulative Reasoning in Propositional Logic using Coq“
Abstract:
Unlike conventional proofs, interactive proof assistants are used to fully formalize proofs and make them machine-verifiable and exchangeable. This work is dedicated to the
attempt of formalizing Theorem 3.25 and the semi-mechanical proving of the Representation Theorem for cumulative reasoning by Kraus, Lehmann, and Magidor[1] using Coq[2]. The work primarily focuses on the case of cumulative reasoning based on propositional
logic. The Representation Theorem for cumulative reasoning by Kraus, Lehmann, and Magidor (KLM Theorem) is one of the fundamental theorems in the field of non-monotonic logic. The theorem establishes a connection between the syntactic level of rules and properties
of cumulative consequence relations and the semantic level described by cumulative models. Informally speaking, the KLM Theorem states that a consequence relation is cumulative if and only if it can be defined by a cumulative model. This equivalence forms
the theoretical basis for cumulative logic and ensures a correct representation of cumulative consequence relations through both syntactic descriptions (such as reflexivity, left logical equivalence, right weakening, cut, and cautious monotonicity) and through
a consistent semantic interpretation. Conversely, the theorem ensures that any relation defined by a cumulative model corresponds to these mentioned syntactic rules.
References
[1] Sarit Kraus, Daniel Lehmann, and Menachem Magidor. Nonmonotonic reasoning, preferential models, and cumulative logics.
Artificial Intelligence, 44(1):167–207, 1990.
[2] Coq Team. Introduction the coq proof assistant
https://coq.inria.fr/doc/v8.7.2/refman/introduction.html.
**We cordially ask the attendees to turn on their cameras and turn off their microphones during the presentation.
---
Current Scheduled Talks ----
If you do not wish to receive messages from this mailing list anymore, please let me know by simply responding „unsubscribe“ to this mail (steffi.bluemel@fernuni-hagen.de).
Best regards,
Steffi Blümel
- Sekretariat -
----------------------------------------------------
FernUniversität in Hagen
Fakultät Mathematik und Informatik /
Lehrgebiet Künstliche Intelligenz
Universitätsstraße 1
58097 Hagen
Fon: + 49 23 31 - 9 87 40 06
E-Mail:
steffi.bluemel@fernuni-hagen.de