A Natural Proof System for Herbrand's Theorem

Benjamin Ralph

doi:10.1007/978-3-319-72056-2_18

A Natural Proof System for Herbrand's Theorem

Research output: Chapter or section in a book/report/conference proceeding › Chapter in a published conference proceeding

2 Citations (SciVal)

Abstract

The reduction of undecidable first-order logic to decidable
propositional logic via Herbrand’s theorem has long been of interest to
theoretical computer science, with the notion of a Herbrand proof motivating
the definition of expansion proofs. The problem of building a natural
proof system around expansion proofs, with composition of proofs
and cut-free completeness, has been approached from a variety of different
angles. In this paper we construct a simple deep inference system
for first-order logic, KSh2, based around the notion of expansion proofs,
as a starting point to developing a rich proof theory around this foundation.
Translations between proofs in this system and expansion proofs
are given, retaining much of the structure in each direction.

Original language	English
Title of host publication	Logical Foundations of Computer Science - International Symposium, LFCS 2018, Proceedings
Editors	Anil Nerode, Sergei Artemov
Publisher	Springer
Pages	289-308
Number of pages	20
ISBN (Print)	9783319720555
DOIs	https://doi.org/10.1007/978-3-319-72056-2_18
Publication status	Published - 2018

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	10703

Keywords

Deep inference
Expansion proofs
First-order logic
Herbrand’s theorem
Structural proof theory

ASJC Scopus subject areas

Theoretical Computer Science
General Computer Science

Access to Document

10.1007/978-3-319-72056-2_18

Efficient and Natural Proof Systems
Guglielmi, A. (PI), Bruscoli, P. (CoI) & McCusker, G. (CoI)
Engineering and Physical Sciences Research Council
1/02/13 → 12/05/16
Project: Research council

Cite this

Ralph, B. (2018). A Natural Proof System for Herbrand's Theorem. In A. Nerode, & S. Artemov (Eds.), Logical Foundations of Computer Science - International Symposium, LFCS 2018, Proceedings (pp. 289-308). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10703). Springer. https://doi.org/10.1007/978-3-319-72056-2_18

A Natural Proof System for Herbrand's Theorem. / Ralph, Benjamin.
Logical Foundations of Computer Science - International Symposium, LFCS 2018, Proceedings. ed. / Anil Nerode; Sergei Artemov. Springer, 2018. p. 289-308 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10703).

Research output: Chapter or section in a book/report/conference proceeding › Chapter in a published conference proceeding

Ralph, B 2018, A Natural Proof System for Herbrand's Theorem. in A Nerode & S Artemov (eds), Logical Foundations of Computer Science - International Symposium, LFCS 2018, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 10703, Springer, pp. 289-308. https://doi.org/10.1007/978-3-319-72056-2_18

Ralph B. A Natural Proof System for Herbrand's Theorem. In Nerode A, Artemov S, editors, Logical Foundations of Computer Science - International Symposium, LFCS 2018, Proceedings. Springer. 2018. p. 289-308. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). Epub 2017 Nov 28. doi: 10.1007/978-3-319-72056-2_18

@inproceedings{a5ca65def2c9455fbbc5ff4466555ce2,

title = "A Natural Proof System for Herbrand's Theorem",

abstract = "The reduction of undecidable first-order logic to decidablepropositional logic via Herbrand{\textquoteright}s theorem has long been of interest totheoretical computer science, with the notion of a Herbrand proof motivatingthe definition of expansion proofs. The problem of building a naturalproof system around expansion proofs, with composition of proofsand cut-free completeness, has been approached from a variety of differentangles. In this paper we construct a simple deep inference systemfor first-order logic, KSh2, based around the notion of expansion proofs,as a starting point to developing a rich proof theory around this foundation.Translations between proofs in this system and expansion proofsare given, retaining much of the structure in each direction.",

keywords = "Deep inference, Expansion proofs, First-order logic, Herbrand{\textquoteright}s theorem, Structural proof theory",

author = "Benjamin Ralph",

year = "2018",

doi = "10.1007/978-3-319-72056-2_18",

language = "English",

isbn = "9783319720555",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer",

pages = "289--308",

editor = "Anil Nerode and Sergei Artemov",

booktitle = "Logical Foundations of Computer Science - International Symposium, LFCS 2018, Proceedings",

}

TY - GEN

T1 - A Natural Proof System for Herbrand's Theorem

AU - Ralph, Benjamin

PY - 2018

Y1 - 2018

N2 - The reduction of undecidable first-order logic to decidablepropositional logic via Herbrand’s theorem has long been of interest totheoretical computer science, with the notion of a Herbrand proof motivatingthe definition of expansion proofs. The problem of building a naturalproof system around expansion proofs, with composition of proofsand cut-free completeness, has been approached from a variety of differentangles. In this paper we construct a simple deep inference systemfor first-order logic, KSh2, based around the notion of expansion proofs,as a starting point to developing a rich proof theory around this foundation.Translations between proofs in this system and expansion proofsare given, retaining much of the structure in each direction.

AB - The reduction of undecidable first-order logic to decidablepropositional logic via Herbrand’s theorem has long been of interest totheoretical computer science, with the notion of a Herbrand proof motivatingthe definition of expansion proofs. The problem of building a naturalproof system around expansion proofs, with composition of proofsand cut-free completeness, has been approached from a variety of differentangles. In this paper we construct a simple deep inference systemfor first-order logic, KSh2, based around the notion of expansion proofs,as a starting point to developing a rich proof theory around this foundation.Translations between proofs in this system and expansion proofsare given, retaining much of the structure in each direction.

KW - Deep inference

KW - Expansion proofs

KW - First-order logic

KW - Herbrand’s theorem

KW - Structural proof theory

U2 - 10.1007/978-3-319-72056-2_18

DO - 10.1007/978-3-319-72056-2_18

M3 - Chapter in a published conference proceeding

SN - 9783319720555

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 289

EP - 308

BT - Logical Foundations of Computer Science - International Symposium, LFCS 2018, Proceedings

A2 - Nerode, Anil

A2 - Artemov, Sergei

PB - Springer

ER -

A Natural Proof System for Herbrand's Theorem

Abstract

Publication series

Keywords

ASJC Scopus subject areas

Access to Document

Fingerprint

Projects

Efficient and Natural Proof Systems

Cite this