Substitutionless First-Order Logic: A Formal Soundness Proof

Andreas Halkjær From, John Bruntse Larsen, Anders Schlichtkrull, Jørgen Villadsen

Research output: Contribution to conferencePaperResearchpeer-review

248 Downloads (Orbit)

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
Country/TerritoryUnited 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