Formal verification of logical calculi and simulations in Isabelle/HOL

Abstract

This thesis 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 completeness (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. Finally, I formalized three interpreters for dynamically typed bytecode languages. The first one serves as a baseline, and the other two add speculative optimizations. I proved that the first interpreter can simulate the second one and vice versa, and also that the second interpreter can simulate the third one and vice versa. This formalization was also done using my framework for simulation proofs. All formalizations were carried out using the Isabelle/HOL proof assistant.

Diese Dissertation beschreibt meine Formalisierungen von drei Kalkülen: SCL(FOL), Geordnete Grundresolution, und Grundsuperposition. Die formalisierten Haupttheoreme sind Korrektheit (d.h., jede durch den Kalkül von gültigen Formeln abgeleitete Formel ist selbst gültig) und Widerspruchsvollständigkeit (d.h., aus einer unerfüll- baren Formel kann der Kalkül einen Widerspruch ableiten). Für SCL(FOL) ist ein weiteres Haupttheorem, dass jede abgeleitete Formel nicht redundant ist (d.h., sie folgt nicht „trivialerweise“ aus bereits bekannten Formeln). Geordnete Grundresolution genießt diese letzte Eigenschaft nur dann, wenn eine geeignete Strategie Anwendung findet. Ich bewies das bereits bekannte Ergebnis erneut und formalisierte, dass eine spezifische Strategie für SCL(FOL) eine spezifische Strategie für Geordnete Grundresolution simulieren kann und umgekehrt. Dies wurde mithilfe eines von mir entwickelten Frameworks für Simulationsbeweise durchgeführt. Abschließend formalisierte ich drei Interpreter für dynamisch typisierte Bytecodesprachen. Der Erste dient als Vergleichsbasis und die Anderen fügen spekulative Optimierungen hinzu. Ich bewies, dass der Erste den Zweiten simulieren kann und umgekehrt sowie dass der Zweite den Dritten simulieren kann und umgekehrt. Dies wurde ebenfalls mithilfe meines Frameworks für Simulationsbeweise durchgeführt. Sämtliche Formalisierungen wurden mithilfe des Beweisassistenten Isabelle/HOL durchgeführt.