A Systematic Approach to Canonicity in the Classical Sequent Calculus

Kaustuv Chaudhuri 1 Stefan Hetzl 1 Dale Miller 1, 2
1 PARSIFAL - Proof search and reasoning with logic specifications
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France, X - École polytechnique, CNRS - Centre National de la Recherche Scientifique : UMR7161
Abstract : The sequent calculus is often criticized for requiring proofs to contain large amounts of low-level syntactic details that can obscure the essence of a given proof. Because each inference rule introduces only a single connective, sequent proofs can separate closely related steps---such as instantiating a block of quantifiers---by irrelevant noise. Moreover, the sequential nature of sequent proofs forces proof steps that are syntactically non-interfering and permutable to nevertheless be written in some arbitrary order. The sequent calculus thus lacks a notion of canonicity: proofs that should be considered essentially the same may not have a common syntactic form. To fix this problem, many researchers have proposed replacing the sequent calculus with proof structures that are more parallel or geometric. Proof-nets, matings, and atomic flows are examples of such revolutionary formalisms. We propose, instead, an evolutionary approach to recover canonicity within the sequent calculus, which we illustrate for classical first-order logic. The essential element of our approach is the use of a multi-focused sequent calculus as the means of abstracting away the details from classical cut-free sequent proofs. We show that, among the multi-focused proofs, the maximally multi-focused proofs that make the foci as parallel as possible are canonical. Moreover, such proofs are isomorphic to expansion proofs---a well known, minimalistic, and parallel generalization of Herbrand disjunctions---for classical first-order logic. This technique is a systematic way to recover the desired essence of any sequent proof without abandoning the sequent calculus.
Type de document :
Communication dans un congrès
Patrick Cégielski and Arnaud Durand. 21st EACSL Annual Conference on Computer Science Logic, Sep 2012, Fontainebleau, France. 16, pp.183-197, 2012, Leibniz International Proceedings in Informatics (LIPIcs). 〈10.4230/LIPIcs.CSL.2012.183〉
Liste complète des métadonnées

Littérature citée [30 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-00772396
Contributeur : Kaustuv Chaudhuri <>
Soumis le : jeudi 10 janvier 2013 - 14:31:21
Dernière modification le : mercredi 25 avril 2018 - 10:45:27
Document(s) archivé(s) le : jeudi 11 avril 2013 - 04:05:42

Fichiers

lkfexp.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Kaustuv Chaudhuri, Stefan Hetzl, Dale Miller. A Systematic Approach to Canonicity in the Classical Sequent Calculus. Patrick Cégielski and Arnaud Durand. 21st EACSL Annual Conference on Computer Science Logic, Sep 2012, Fontainebleau, France. 16, pp.183-197, 2012, Leibniz International Proceedings in Informatics (LIPIcs). 〈10.4230/LIPIcs.CSL.2012.183〉. 〈hal-00772396〉

Partager

Métriques

Consultations de la notice

366

Téléchargements de fichiers

116