On Combinatorial Proofs for Logics of Relevance and Entailment

Matteo Acclavio (1, 2) , Lutz Strassburger (2, 3, 4)

1 ROMA TRE - Università degli Studi Roma Tre = Roma Tre University
2 PARSIFAL - Proof search and reasoning with logic specifications
3 LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau]
4 PARTOUT - Automatisation et ReprésenTation: fOndation du calcUl et de la déducTion

Hughes' combinatorial proofs give canonical representations for classical logic proofs. In this paper we characterize classical combi-natorial proofs which also represent valid proofs for relevant logic with and without the mingle axiom. Moreover, we extend our syntax in order to represent combinatorial proofs for the more restrictive framework of entailment logic.

Mots clés: Relevant Logic; Combinatorial Proofs; Shew fibrations; Entailment Logic; Proof Theory

Domaines: Logique en informatique [cs.LO]

Matteo Acclavio, Lutz Strassburger. On Combinatorial Proofs for Logics of Relevance and Entailment. WoLLIC 2019 - 26th International Workshop on Logic, Language, Information, and Computation, Jul 2019, Utrecht, Netherlands. pp.1-16, ⟨10.1007/978-3-662-59533-6_1⟩. ⟨hal-02390426⟩