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 publicationSymposium on Logical Foundations in Computer Science 2018
EditorsSergei Artemov, Anil Nerode
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

  • proof theory
  • deep inference
  • expansion proofs
  • structural proof theory
  • Herbrand's theorem

Cite this

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

A Natural Proof System for Herbrand's Theorem. / Ralph, Benjamin.

Symposium on Logical Foundations in Computer Science 2018. ed. / Sergei Artemov; Anil Nerode. 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 S Artemov & A Nerode (eds), Symposium on Logical Foundations in Computer Science 2018. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 10703, Springer, pp. 289-308. DOI: 10.1007/978-3-319-72056-2_18
Ralph B. A Natural Proof System for Herbrand's Theorem. In Artemov S, Nerode A, editors, Symposium on Logical Foundations in Computer Science 2018. Springer. 2018. p. 289-308. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). Available from, DOI: 10.1007/978-3-319-72056-2_18
Ralph, Benjamin. / A Natural Proof System for Herbrand's Theorem. Symposium on Logical Foundations in Computer Science 2018. editor / Sergei Artemov ; Anil Nerode. 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 = "proof theory, deep inference, expansion proofs, structural proof theory, Herbrand's theorem",
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 = "Sergei Artemov and Anil Nerode",
booktitle = "Symposium on Logical Foundations in Computer Science 2018",

}

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 - proof theory

KW - deep inference

KW - expansion proofs

KW - structural proof theory

KW - Herbrand's theorem

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 - Symposium on Logical Foundations in Computer Science 2018

PB - Springer

ER -