Campus Event Calendar
Event Entry
What and Who
Formal Verification of Logical Calculi and Simulations in Isabelle/HOL
Martin Desharnais
Max-Planck-Institut für Informatik - RG 1
Promotionskolloquium
AG 1, AG 2, AG 3, INET, AG 4, AG 5, D6, SWS, RG1, MMCI
Public Audience
English
Note: We use this to send email in the morning.
Date, Time and Location
Wednesday, 29 January 2025
14:00
90 Minutes
E1 4
024
Saarbrücken
Abstract
This thesis defense describes my formalizations of three proof calculi: SCL(FOL), ground ordered resolution, and ground superposition. The main theorems formalized for each calculus are soundness (i.e., every formula derived from valid formulas is valid) and refutational com-pleteness (i.e., if a formula is invalid, then the calculus can be used to derive a refutation). For SCL(FOL), another main theorem is that derived formulas are nonredundant (i.e., they are not “obvious” from the already known formulas).
Ground ordered resolution only has this last property when a suitable strategy is used. I re-proved and formalized a previously known result that a specific strategy for SCL(FOL) can simulate a specific strategy for ground ordered resolution and vice versa. This was carried out with a framework for simulation proofs that I developed. All formalizations were carried out using the Isabelle/HOL proof assistant.
Ground ordered resolution only has this last property when a suitable strategy is used. I re-proved and formalized a previously known result that a specific strategy for SCL(FOL) can simulate a specific strategy for ground ordered resolution and vice versa. This was carried out with a framework for simulation proofs that I developed. All formalizations were carried out using the Isabelle/HOL proof assistant.
Contact
Jennifer Müller
+49 681 9325 2900
--email hidden
passcode not visible
logged in users only
Jennifer Müller, 01/20/2025 14:39 -- Created document.