Formalized Proof Systems for Propositional Logic

Julius Michaelis; Tobias Nipkow

doi:10.4230/LIPIcs.TYPES.2017.5

Formalized Proof Systems for Propositional Logic

Julius Michaelis, Tobias Nipkow

Informatics 7 - Chair of Theoretical Computer Science

Technical University of Munich

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

13 Scopus citations

Abstract

We have formalized a range of proof systems for classical propositional logic (sequent calculus, natural deduction, Hilbert systems, resolution) in Isabelle/HOL and have proved the most important meta-theoretic results about semantics and proofs: compactness, soundness, completeness, translations between proof systems, cut-elimination, interpolation and model existence.

Original language	English
Title of host publication	23rd International Conference on Types for Proofs and Programs, TYPES 2017
Editors	Ambrus Kaposi
Publisher	Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
ISBN (Electronic)	9783959770712
DOIs	https://doi.org/10.4230/LIPIcs.TYPES.2017.5
State	Published - 2017
Event	23rd International Conference on Types for Proofs and Programs, TYPES 2017 - Budapest, Hungary Duration: 29 May 2017 → 1 Jun 2017

Publication series

Name	Leibniz International Proceedings in Informatics, LIPIcs
Volume	104
ISSN (Print)	1868-8969

Conference

Conference	23rd International Conference on Types for Proofs and Programs, TYPES 2017
Country/Territory	Hungary
City	Budapest
Period	29/05/17 → 1/06/17

Keywords

formalization of logic
natural deduction
proof systems
resolution
sequent calculus

Access to Document

10.4230/LIPIcs.TYPES.2017.5

Cite this

Michaelis, J., & Nipkow, T. (2017). Formalized Proof Systems for Propositional Logic. In A. Kaposi (Ed.), 23rd International Conference on Types for Proofs and Programs, TYPES 2017 Article 5 (Leibniz International Proceedings in Informatics, LIPIcs; Vol. 104). Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing. https://doi.org/10.4230/LIPIcs.TYPES.2017.5

@inproceedings{7b261249387a46d6b19bcbcd47f533e2,

title = "Formalized Proof Systems for Propositional Logic",

abstract = "We have formalized a range of proof systems for classical propositional logic (sequent calculus, natural deduction, Hilbert systems, resolution) in Isabelle/HOL and have proved the most important meta-theoretic results about semantics and proofs: compactness, soundness, completeness, translations between proof systems, cut-elimination, interpolation and model existence.",

keywords = "formalization of logic, natural deduction, proof systems, resolution, sequent calculus",

author = "Julius Michaelis and Tobias Nipkow",

note = "Publisher Copyright: {\textcopyright} 2020 Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing. All rights reserved.; 23rd International Conference on Types for Proofs and Programs, TYPES 2017 ; Conference date: 29-05-2017 Through 01-06-2017",

year = "2017",

doi = "10.4230/LIPIcs.TYPES.2017.5",

language = "English",

series = "Leibniz International Proceedings in Informatics, LIPIcs",

publisher = "Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing",

editor = "Ambrus Kaposi",

booktitle = "23rd International Conference on Types for Proofs and Programs, TYPES 2017",

}

Michaelis, J & Nipkow, T 2017, Formalized Proof Systems for Propositional Logic. in A Kaposi (ed.), 23rd International Conference on Types for Proofs and Programs, TYPES 2017., 5, Leibniz International Proceedings in Informatics, LIPIcs, vol. 104, Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, 23rd International Conference on Types for Proofs and Programs, TYPES 2017, Budapest, Hungary, 29/05/17. https://doi.org/10.4230/LIPIcs.TYPES.2017.5

Formalized Proof Systems for Propositional Logic. / Michaelis, Julius; Nipkow, Tobias.
23rd International Conference on Types for Proofs and Programs, TYPES 2017. ed. / Ambrus Kaposi. Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, 2017. 5 (Leibniz International Proceedings in Informatics, LIPIcs; Vol. 104).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - Formalized Proof Systems for Propositional Logic

AU - Michaelis, Julius

AU - Nipkow, Tobias

PY - 2017

Y1 - 2017

N2 - We have formalized a range of proof systems for classical propositional logic (sequent calculus, natural deduction, Hilbert systems, resolution) in Isabelle/HOL and have proved the most important meta-theoretic results about semantics and proofs: compactness, soundness, completeness, translations between proof systems, cut-elimination, interpolation and model existence.

AB - We have formalized a range of proof systems for classical propositional logic (sequent calculus, natural deduction, Hilbert systems, resolution) in Isabelle/HOL and have proved the most important meta-theoretic results about semantics and proofs: compactness, soundness, completeness, translations between proof systems, cut-elimination, interpolation and model existence.

KW - formalization of logic

KW - natural deduction

KW - proof systems

KW - resolution

KW - sequent calculus

UR - http://www.scopus.com/inward/record.url?scp=85121995807&partnerID=8YFLogxK

U2 - 10.4230/LIPIcs.TYPES.2017.5

DO - 10.4230/LIPIcs.TYPES.2017.5

M3 - Conference contribution

AN - SCOPUS:85121995807

T3 - Leibniz International Proceedings in Informatics, LIPIcs

BT - 23rd International Conference on Types for Proofs and Programs, TYPES 2017

A2 - Kaposi, Ambrus

PB - Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing

T2 - 23rd International Conference on Types for Proofs and Programs, TYPES 2017

Y2 - 29 May 2017 through 1 June 2017

ER -

Formalized Proof Systems for Propositional Logic

Abstract

Publication series

Conference

Keywords

Access to Document

Other files and links

Fingerprint

Cite this