A Natural Proof System for Herbrand's Theorem

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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.
LanguageEnglish
Title of host publicationLogical Foundations of Computer Science - International Symposium, LFCS 2018, Proceedings
EditorsAnil Nerode, Sergei Artemov
PublisherSpringer
Pages289-308
Number of pages20
ISBN (Print)9783319720555
DOIs
StatusPublished - 2018

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume10703

Fingerprint

Proof System
Theorem
First-order Logic
Proof Theory
Propositional Logic
Completeness
Computer Science
Angle

Keywords

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

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

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 in Book/Report/Conference proceedingConference contribution

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)). https://doi.org/10.1007/978-3-319-72056-2_18
Ralph, Benjamin. / A Natural Proof System for Herbrand's Theorem. Logical Foundations of Computer Science - International Symposium, LFCS 2018, Proceedings. editor / Anil Nerode ; Sergei Artemov. Springer, 2018. pp. 289-308 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{a5ca65def2c9455fbbc5ff4466555ce2,
title = "A Natural Proof System for Herbrand's Theorem",
abstract = "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.",
keywords = "Deep inference, Expansion proofs, First-order logic, Herbrand’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 - Conference contribution

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 -