Equality and fixpoints in the calculus of structures

Kaustuv Chaudhuri 1 Nicolas Guenot 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 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.
Type de document :
Communication dans un congrès
Thomas A. Henzinger and Dale Miller. 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. ACM-SIGPLAN, pp.1 - 10, 2014, 〈http://lics.rwth-aachen.de/csl-lics14/〉. 〈10.1145/2603088.2603140〉
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01091570
Contributeur : Kaustuv Chaudhuri <>
Soumis le : vendredi 5 décembre 2014 - 16:20:12
Dernière modification le : jeudi 10 mai 2018 - 02:06:27
Document(s) archivé(s) le : lundi 9 mars 2015 - 06:04:43

Fichiers

eqfix-hal.pdf
Fichiers produits par l'(les) auteur(s)

Licence


Distributed under a Creative Commons Paternité - Pas de modifications 4.0 International License

Identifiants

Collections

Citation

Kaustuv Chaudhuri, Nicolas Guenot. Equality and fixpoints in the calculus of structures. Thomas A. Henzinger and Dale Miller. 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. ACM-SIGPLAN, pp.1 - 10, 2014, 〈http://lics.rwth-aachen.de/csl-lics14/〉. 〈10.1145/2603088.2603140〉. 〈hal-01091570〉

Partager

Métriques

Consultations de la notice

383

Téléchargements de fichiers

93