From Syntactic Proofs to Combinatorial Proofs

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

Abstract

In this paper we investigate Hughes’ combinatorial proofs as a notion of proof identity for classical logic. We show for various syntactic formalisms including sequent calculus, analytic tableaux, and resolution, how they can be translated into combinatorial proofs, and which notion of identity they enforce. This allows the comparison of proofs that are given in different formalisms.

Original languageEnglish
Title of host publicationAutomated Reasoning - 9th International Joint Conference, IJCAR 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings
EditorsRoberto Sebastiani, Didier Galmiche, Stephan Schulz
PublisherSpringer Verlag
Pages481-497
Number of pages17
ISBN (Print)9783319942049
DOIs
Publication statusPublished - 1 Jan 2018
Event9th International Joint Conference on Automated Reasoning, IJCAR 2018 Held as Part of the Federated Logic Conference, FloC 2018 - Oxford, United Kingdom
Duration: 14 Jul 201817 Jul 2018

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume10900 LNAI
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference9th International Joint Conference on Automated Reasoning, IJCAR 2018 Held as Part of the Federated Logic Conference, FloC 2018
Country/TerritoryUnited Kingdom
CityOxford
Period14/07/1817/07/18

Fingerprint

Dive into the research topics of 'From Syntactic Proofs to Combinatorial Proofs'. Together they form a unique fingerprint.

Cite this