Equality and fixpoints in the calculus of structures - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2014

Equality and fixpoints in the calculus of structures

Résumé

The standard proof theory for logics with equality and fixpoints suffers from limitations of the sequent calculus, where reasoning is separated from computational tasks such as unification or rewriting. We propose in this paper an extension of the calculus of structures, a deep inference formalism, that supports incremental and contextual reasoning with equality and fixpoints in the setting of linear logic. This system allows deductive and computational steps to mix freely in a continuum which integrates smoothly into the usual versatile rules of multiplicative-additive linear logic in deep inference.
Fichier principal
Vignette du fichier
eqfix-hal.pdf (245.25 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-01091570 , version 1 (05-12-2014)

Licence

Paternité - Pas de modifications

Identifiants

Citer

Kaustuv Chaudhuri, Nicolas Guenot. Equality and fixpoints in the calculus of structures. JOINT MEETING OF the Twenty-Third EACSL Annual Conference on COMPUTER SCIENCE LOGIC (CSL) AND the Twenty-Ninth Annual ACM/IEEE Symposium on LOGIC IN COMPUTER SCIENCE (LICS), Jul 2014, Vienna, Austria. pp.1 - 10, ⟨10.1145/2603088.2603140⟩. ⟨hal-01091570⟩
639 Consultations
207 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More