Projects per year
Abstract
The reduction of undecidable firstorder 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 cutfree completeness, has been approached from a variety of different
angles. In this paper we construct a simple deep inference system
for firstorder 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.
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 cutfree completeness, has been approached from a variety of different
angles. In this paper we construct a simple deep inference system
for firstorder 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  289308 
Number of pages  20 
ISBN (Print)  9783319720555 
DOIs  
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
 Firstorder logic
 Herbrand’s theorem
 Structural proof theory
ASJC Scopus subject areas
 Theoretical Computer Science
 General Computer Science
Fingerprint
Dive into the research topics of 'A Natural Proof System for Herbrand's Theorem'. Together they form a unique fingerprint.Projects
 1 Finished

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