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. Zoom Room: https://eur05.safelinks.protection.outlook.com/?url=https%3A%2F%2Ffernuni-hagen.zoom.us%2Fj%2F62388524887%3Fpwd%3DWmJRRUpDZWZ4WlJoeFlGQTBESWplQT09&data=05%7C02%7Csteffi.bluemel%40fernuni-hagen.de%7C42fe776c1f324ba6b7aa08dc223844de%7Cc2bba033db424b299adb6ac379499ef7%7C1%7C0%7C638422872265614676%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C0%7C%7C%7C&sdata=X%2F4UFs7fFH%2BIDLw7SsgOOqv3FUyNoCPE7k9B7YFDaGE%3D&reserved=0<https://fernuni-hagen.zoom.us/j/62388524887?pwd=WmJRRUpDZWZ4WlJoeFlGQTBESWplQT09> --- Current Scheduled Talks ---- * 20th February, Jonathan Walther, BSc proposal * 6th March, Andy Schmidt, BSc proposal * 13th March, Marcel Traser, MSc proposal * 20th March, Jean-Guy Mailly, invited speaker 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<mailto: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<mailto:steffi.bluemel@fernuni-hagen.de>