FLOC 2018: FEDERATED LOGIC CONFERENCE 2018
Deep Inference, Herbrand's Theorem and Expansion Proofs

Author: Benjamin Ralph

Paper Information

Title:Deep Inference, Herbrand's Theorem and Expansion Proofs
Authors:Benjamin Ralph
Proceedings:TYDI-0 Abstracts
Editor: Lutz Stra├čburger
Keywords:structural proof theory, first-order logic, deep inference, Herbrand's theorem, expansion proofs
Abstract:

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, a compositional formalism that expresses the strictly first-order content of a proof. Recently, a simple deep inference system for first-order logic, KSh2, has been constructed based around the notion of expansion proofs, as a starting point to developing a rich proof theory around this foundation. This abstract summarises the author's recent paper, with a slight change of focus due to the nature of the workshop.

Pages:3
Talk:Jul 07 15:00 (Session 28N: Medial)
Paper: