A Natural Proof System for Herbrand's Theorem

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

2 Citations (SciVal)


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 languageEnglish
Title of host publicationLogical Foundations of Computer Science - International Symposium, LFCS 2018, Proceedings
EditorsAnil Nerode, Sergei Artemov
Number of pages20
ISBN (Print)9783319720555
Publication statusPublished - 2018

Publication series

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


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

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)


Dive into the research topics of 'A Natural Proof System for Herbrand's Theorem'. Together they form a unique fingerprint.

Cite this