Substitutionless First-Order Logic: A Formal Soundness Proof
Authors: Andreas Halkjær From, John Bruntse Larsen, Anders Schlichtkrull and Jørgen Villadsen
Paper Information
| Title: | Substitutionless First-Order Logic: A Formal Soundness Proof |
| Authors: | Andreas Halkjær From, John Bruntse Larsen, Anders Schlichtkrull and Jørgen Villadsen |
| Proceedings: | Isabelle Papers |
| Editor: | Makarius Wenzel |
| Keywords: | First-Order Logic, Substitution, Soundness, Proof System, Formalization |
| Abstract: | ABSTRACT. Substitution under quantifiers is non-trivial and may obscure a proof system for newcomers. Monk (Arch. Math. Log. Grundl. 1965) successfully eliminates substitution via identities and also uses a so-called normalization of formulas as a further simplification. We formalize the substitutionless proof system in Isabelle/HOL, spelling out its side conditions explicitly and verifying its soundness. |
| Pages: | 3 |
| Talk: | Jul 13 16:00 (Session 88C: Isabelle 4) |
| Paper: |  |