Conference paper
Substitutionless First-Order Logic: A Formal Soundness Proof
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
Language: | English |
---|---|
Year: | 2018 |
Proceedings: | Isabelle Workshop 2018 |
Types: | Conference paper |
ORCIDs: | From, Andreas Halkjær , Larsen, John Bruntse , Schlichtkrull, Anders and Villadsen, Jørgen |