Substitutionless First-Order Logic: A Formal Soundness Proof

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

Substitutionless First-Order Logic: A Formal Soundness Proof

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

Department of Applied Mathematics and Computer Science

Research output: Contribution to conference › Paper › Research › peer-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 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	http://sketis.net/isabelle/isabelle-workshop-2018

Access to Document

Substitutionless First Order LogicFinal published version, 128 KB

OpenUrl availability

Full text

Cite this

@conference{f92eecb6be2e40b586c67cf887b629bf,

title = "Substitutionless First-Order Logic: A Formal Soundness Proof",

abstract = "Substitution under quantifiers is non-trivial and may obscure a proof system for newcomers. Monk (Arch. Math. Log. Grundl. 1965) successfully eliminatessubstitution 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",

author = "From, {Andreas Halkj{\ae}r} and Larsen, {John Bruntse} and Anders Schlichtkrull and J{\o}rgen Villadsen",

year = "2018",

language = "English",

note = "Isabelle Workshop 2018 ; Conference date: 13-07-2018 Through 13-07-2018",

url = "http://sketis.net/isabelle/isabelle-workshop-2018",

}

TY - CONF

T1 - Substitutionless First-Order Logic: A Formal Soundness Proof

AU - From, Andreas Halkjær

AU - Larsen, John Bruntse

AU - Schlichtkrull, Anders

AU - Villadsen, Jørgen

PY - 2018

Y1 - 2018

N2 - Substitution under quantifiers is non-trivial and may obscure a proof system for newcomers. Monk (Arch. Math. Log. Grundl. 1965) successfully eliminatessubstitution 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

AB - Substitution under quantifiers is non-trivial and may obscure a proof system for newcomers. Monk (Arch. Math. Log. Grundl. 1965) successfully eliminatessubstitution 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

M3 - Paper

T2 - Isabelle Workshop 2018

Y2 - 13 July 2018 through 13 July 2018

ER -

Substitutionless First-Order Logic: A Formal Soundness Proof

Abstract

Workshop

Access to Document

OpenUrl availability

Fingerprint

Cite this