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: |