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
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
Original language | English |
---|---|
Publication date | 2018 |
Number of pages | 3 |
Publication status | Published - 2018 |
Event | Isabelle Workshop 2018 - Oxford, United Kingdom Duration: 13 Jul 2018 → 13 Jul 2018 http://sketis.net/isabelle/isabelle-workshop-2018 |
Workshop
Workshop | Isabelle Workshop 2018 |
---|---|
Country/Territory | United Kingdom |
City | Oxford |
Period | 13/07/2018 → 13/07/2018 |
Internet address |