Substitutionless First-Order Logic: A Formal Soundness Proof

Research output: Contribution to conferencePaperResearchpeer-review

128 Downloads (Pure)

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
Original languageEnglish
Publication date2018
Number of pages3
Publication statusPublished - 2018
EventIsabelle Workshop 2018 - Oxford, United Kingdom
Duration: 13 Jul 201813 Jul 2018
http://sketis.net/isabelle/isabelle-workshop-2018

Workshop

WorkshopIsabelle Workshop 2018
CountryUnited Kingdom
CityOxford
Period13/07/201813/07/2018
Internet address

Fingerprint Dive into the research topics of 'Substitutionless First-Order Logic: A Formal Soundness Proof'. Together they form a unique fingerprint.

Cite this