Quasipolynomial Normalisation in Deep Inference via Atomic Flows and Threshold Formulae
Identifieur interne : 003292 ( Main/Exploration ); précédent : 003291; suivant : 003293Quasipolynomial Normalisation in Deep Inference via Atomic Flows and Threshold Formulae
Auteurs : Paola Bruscoli [France] ; Alessio Guglielmi [France] ; Tom Gundersen [France] ; Michel Parigot [France]Source :
Abstract
Jerábek showed that analytic propositional-logic deep-inference proofs can be constructed in quasipolynomial time from nonanalytic proofs. In this work, we improve on that as follows: 1) we significantly simplify the technique; 2) our normalisation procedure is direct, i.e., it is internal to deep inference. The paper is self-contained, and provides a starting point and a good deal of information for tackling the problem of whether a polynomial-time normalisation procedure exists.
Url:
Affiliations:
- France
- Grand Est, Lorraine (région)
- Nancy
- Institut national polytechnique de Lorraine, Université Nancy 2, Université de Lorraine
Links toward previous steps (curation, corpus...)
- to stream Hal, to step Corpus: 003E87
- to stream Hal, to step Curation: 003E87
- to stream Hal, to step Checkpoint: 002916
- to stream Main, to step Merge: 003372
- to stream Main, to step Curation: 003292
Le document en format XML
<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en">Quasipolynomial Normalisation in Deep Inference via Atomic Flows and Threshold Formulae</title><author><name sortKey="Bruscoli, Paola" sort="Bruscoli, Paola" uniqKey="Bruscoli P" first="Paola" last="Bruscoli">Paola Bruscoli</name><affiliation wicri:level="1"><hal:affiliation type="researchteam" xml:id="struct-2347" status="OLD"><idno type="RNSR">199618306V</idno><orgName>Linear logic, proof networks and categorial grammars</orgName><orgName type="acronym">CALLIGRAMME</orgName><desc><address><country key="FR"></country></address><ref type="url">http://www.inria.fr/equipes/calligramme</ref></desc><listRelation><relation active="#struct-160" type="direct"></relation><relation name="UMR7503" active="#struct-441569" type="indirect"></relation><relation active="#struct-300009" type="indirect"></relation><relation active="#struct-300291" type="indirect"></relation><relation active="#struct-300292" type="indirect"></relation><relation active="#struct-300293" type="indirect"></relation><relation active="#struct-2496" type="direct"></relation></listRelation><tutelles><tutelle active="#struct-160" type="direct"><org type="laboratory" xml:id="struct-160" status="OLD"><orgName>Laboratoire Lorrain de Recherche en Informatique et ses Applications</orgName><orgName type="acronym">LORIA</orgName><desc><address><addrLine>Campus Scientifique BP 239 54506 Vandoeuvre-lès-Nancy Cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.loria.fr</ref></desc><listRelation><relation name="UMR7503" active="#struct-441569" type="direct"></relation><relation active="#struct-300009" type="direct"></relation><relation active="#struct-300291" type="direct"></relation><relation active="#struct-300292" type="direct"></relation><relation active="#struct-300293" type="direct"></relation></listRelation></org></tutelle><tutelle name="UMR7503" active="#struct-441569" type="indirect"><org type="institution" xml:id="struct-441569" status="VALID"><idno type="ISNI">0000000122597504</idno><idno type="IdRef">02636817X</idno><orgName>Centre National de la Recherche Scientifique</orgName><orgName type="acronym">CNRS</orgName><date type="start">1939-10-19</date><desc><address><country key="FR"></country></address><ref type="url">http://www.cnrs.fr/</ref></desc></org></tutelle><tutelle active="#struct-300009" type="indirect"><org type="institution" xml:id="struct-300009" status="VALID"><orgName>Institut National de Recherche en Informatique et en Automatique</orgName><orgName type="acronym">Inria</orgName><desc><address><addrLine>Domaine de VoluceauRocquencourt - BP 10578153 Le Chesnay Cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.inria.fr/en/</ref></desc></org></tutelle><tutelle active="#struct-300291" type="indirect"><org type="institution" xml:id="struct-300291" status="OLD"><orgName>Université Henri Poincaré - Nancy 1</orgName><orgName type="acronym">UHP</orgName><date type="end">2011-12-31</date><desc><address><addrLine>24-30 rue Lionnois, BP 60120, 54 003 NANCY cedex, France</addrLine><country key="FR"></country></address></desc></org></tutelle><tutelle active="#struct-300292" type="indirect"><org type="institution" xml:id="struct-300292" status="OLD"><orgName>Université Nancy 2</orgName><date type="end">2011-12-31</date><desc><address><addrLine>91 avenue de la Libération, BP 454, 54001 Nancy cedex</addrLine><country key="FR"></country></address></desc></org></tutelle><tutelle active="#struct-300293" type="indirect"><org type="institution" xml:id="struct-300293" status="OLD"><orgName>Institut National Polytechnique de Lorraine</orgName><orgName type="acronym">INPL</orgName><date type="end">2011-12-31</date><desc><address><country key="FR"></country></address></desc></org></tutelle><tutelle active="#struct-2496" type="direct"><org type="laboratory" xml:id="struct-2496" status="OLD"><orgName>INRIA Lorraine</orgName><desc><address><addrLine>615 rue du Jardin Botanique 54600 Villers-lès-Nancy</addrLine><country key="FR"></country></address><ref type="url">http://www.inria.fr/centre-de-recherche-inria/nancy-grand-est</ref></desc><listRelation><relation active="#struct-300009" type="direct"></relation></listRelation></org></tutelle></tutelles></hal:affiliation><country>France</country><placeName><settlement type="city">Nancy</settlement><region type="region" nuts="2">Grand Est</region><region type="old region" nuts="2">Lorraine (région)</region></placeName><orgName type="university">Université Nancy 2</orgName><orgName type="institution" wicri:auto="newGroup">Université de Lorraine</orgName><placeName><settlement type="city">Nancy</settlement><region type="region" nuts="2">Grand Est</region><region type="old region" nuts="2">Lorraine (région)</region></placeName><orgName type="university">Institut national polytechnique de Lorraine</orgName><orgName type="institution" wicri:auto="newGroup">Université de Lorraine</orgName></affiliation></author><author><name sortKey="Guglielmi, Alessio" sort="Guglielmi, Alessio" uniqKey="Guglielmi A" first="Alessio" last="Guglielmi">Alessio Guglielmi</name><affiliation wicri:level="1"><hal:affiliation type="researchteam" xml:id="struct-2347" status="OLD"><idno type="RNSR">199618306V</idno><orgName>Linear logic, proof networks and categorial grammars</orgName><orgName type="acronym">CALLIGRAMME</orgName><desc><address><country key="FR"></country></address><ref type="url">http://www.inria.fr/equipes/calligramme</ref></desc><listRelation><relation active="#struct-160" type="direct"></relation><relation name="UMR7503" active="#struct-441569" type="indirect"></relation><relation active="#struct-300009" type="indirect"></relation><relation active="#struct-300291" type="indirect"></relation><relation active="#struct-300292" type="indirect"></relation><relation active="#struct-300293" type="indirect"></relation><relation active="#struct-2496" type="direct"></relation></listRelation><tutelles><tutelle active="#struct-160" type="direct"><org type="laboratory" xml:id="struct-160" status="OLD"><orgName>Laboratoire Lorrain de Recherche en Informatique et ses Applications</orgName><orgName type="acronym">LORIA</orgName><desc><address><addrLine>Campus Scientifique BP 239 54506 Vandoeuvre-lès-Nancy Cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.loria.fr</ref></desc><listRelation><relation name="UMR7503" active="#struct-441569" type="direct"></relation><relation active="#struct-300009" type="direct"></relation><relation active="#struct-300291" type="direct"></relation><relation active="#struct-300292" type="direct"></relation><relation active="#struct-300293" type="direct"></relation></listRelation></org></tutelle><tutelle name="UMR7503" active="#struct-441569" type="indirect"><org type="institution" xml:id="struct-441569" status="VALID"><idno type="ISNI">0000000122597504</idno><idno type="IdRef">02636817X</idno><orgName>Centre National de la Recherche Scientifique</orgName><orgName type="acronym">CNRS</orgName><date type="start">1939-10-19</date><desc><address><country key="FR"></country></address><ref type="url">http://www.cnrs.fr/</ref></desc></org></tutelle><tutelle active="#struct-300009" type="indirect"><org type="institution" xml:id="struct-300009" status="VALID"><orgName>Institut National de Recherche en Informatique et en Automatique</orgName><orgName type="acronym">Inria</orgName><desc><address><addrLine>Domaine de VoluceauRocquencourt - BP 10578153 Le Chesnay Cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.inria.fr/en/</ref></desc></org></tutelle><tutelle active="#struct-300291" type="indirect"><org type="institution" xml:id="struct-300291" status="OLD"><orgName>Université Henri Poincaré - Nancy 1</orgName><orgName type="acronym">UHP</orgName><date type="end">2011-12-31</date><desc><address><addrLine>24-30 rue Lionnois, BP 60120, 54 003 NANCY cedex, France</addrLine><country key="FR"></country></address></desc></org></tutelle><tutelle active="#struct-300292" type="indirect"><org type="institution" xml:id="struct-300292" status="OLD"><orgName>Université Nancy 2</orgName><date type="end">2011-12-31</date><desc><address><addrLine>91 avenue de la Libération, BP 454, 54001 Nancy cedex</addrLine><country key="FR"></country></address></desc></org></tutelle><tutelle active="#struct-300293" type="indirect"><org type="institution" xml:id="struct-300293" status="OLD"><orgName>Institut National Polytechnique de Lorraine</orgName><orgName type="acronym">INPL</orgName><date type="end">2011-12-31</date><desc><address><country key="FR"></country></address></desc></org></tutelle><tutelle active="#struct-2496" type="direct"><org type="laboratory" xml:id="struct-2496" status="OLD"><orgName>INRIA Lorraine</orgName><desc><address><addrLine>615 rue du Jardin Botanique 54600 Villers-lès-Nancy</addrLine><country key="FR"></country></address><ref type="url">http://www.inria.fr/centre-de-recherche-inria/nancy-grand-est</ref></desc><listRelation><relation active="#struct-300009" type="direct"></relation></listRelation></org></tutelle></tutelles></hal:affiliation><country>France</country><placeName><settlement type="city">Nancy</settlement><region type="region" nuts="2">Grand Est</region><region type="old region" nuts="2">Lorraine (région)</region></placeName><orgName type="university">Université Nancy 2</orgName><orgName type="institution" wicri:auto="newGroup">Université de Lorraine</orgName><placeName><settlement type="city">Nancy</settlement><region type="region" nuts="2">Grand Est</region><region type="old region" nuts="2">Lorraine (région)</region></placeName><orgName type="university">Institut national polytechnique de Lorraine</orgName><orgName type="institution" wicri:auto="newGroup">Université de Lorraine</orgName></affiliation></author><author><name sortKey="Gundersen, Tom" sort="Gundersen, Tom" uniqKey="Gundersen T" first="Tom" last="Gundersen">Tom Gundersen</name><affiliation wicri:level="1"><hal:affiliation type="laboratory" xml:id="struct-2071" status="VALID"><orgName>Laboratoire d'informatique de l'École polytechnique [Palaiseau]</orgName><orgName type="acronym">LIX</orgName><desc><address><addrLine>Route de Saclay 91128 PALAISEAU CEDEX</addrLine><country key="FR"></country></address><ref type="url">http://www.lix.polytechnique.fr/</ref></desc><listRelation><relation active="#struct-300340" type="direct"></relation><relation name="UMR7161" active="#struct-441569" type="direct"></relation></listRelation><tutelles><tutelle active="#struct-300340" type="direct"><org type="institution" xml:id="struct-300340" status="VALID"><orgName>Polytechnique - X</orgName><desc><address><country key="FR"></country></address></desc></org></tutelle><tutelle name="UMR7161" active="#struct-441569" type="direct"><org type="institution" xml:id="struct-441569" status="VALID"><idno type="ISNI">0000000122597504</idno><idno type="IdRef">02636817X</idno><orgName>Centre National de la Recherche Scientifique</orgName><orgName type="acronym">CNRS</orgName><date type="start">1939-10-19</date><desc><address><country key="FR"></country></address><ref type="url">http://www.cnrs.fr/</ref></desc></org></tutelle></tutelles></hal:affiliation><country>France</country></affiliation></author><author><name sortKey="Parigot, Michel" sort="Parigot, Michel" uniqKey="Parigot M" first="Michel" last="Parigot">Michel Parigot</name><affiliation wicri:level="1"><hal:affiliation type="laboratory" xml:id="struct-1067" status="OLD"><orgName>Preuves, Programmes et Systèmes</orgName><orgName type="acronym">PPS</orgName><date type="end">2015-12-31</date><desc><address><addrLine>Université Paris Diderot, Bât. Sophie Germain, case postale 7014, 75205 Paris Cedex 13</addrLine><country key="FR"></country></address><ref type="url">http://www.pps.univ-paris-diderot.fr</ref></desc><listRelation><relation active="#struct-300301" type="direct"></relation><relation name="UMR7126" active="#struct-441569" type="direct"></relation></listRelation><tutelles><tutelle active="#struct-300301" type="direct"><org type="institution" xml:id="struct-300301" status="VALID"><orgName>Université Paris Diderot - Paris 7</orgName><orgName type="acronym">UP7</orgName><desc><address><addrLine>5 rue Thomas-Mann - 75205 Paris cedex 13</addrLine><country key="FR"></country></address><ref type="url">http://www.univ-paris-diderot.fr</ref></desc></org></tutelle><tutelle name="UMR7126" active="#struct-441569" type="direct"><org type="institution" xml:id="struct-441569" status="VALID"><idno type="ISNI">0000000122597504</idno><idno type="IdRef">02636817X</idno><orgName>Centre National de la Recherche Scientifique</orgName><orgName type="acronym">CNRS</orgName><date type="start">1939-10-19</date><desc><address><country key="FR"></country></address><ref type="url">http://www.cnrs.fr/</ref></desc></org></tutelle></tutelles></hal:affiliation><country>France</country></affiliation></author></titleStmt><publicationStmt><idno type="wicri:source">HAL</idno><idno type="RBID">Hal:inria-00441213</idno><idno type="halId">inria-00441213</idno><idno type="halUri">https://hal.inria.fr/inria-00441213</idno><idno type="url">https://hal.inria.fr/inria-00441213</idno><date when="2009-12-15">2009-12-15</date><idno type="wicri:Area/Hal/Corpus">003E87</idno><idno type="wicri:Area/Hal/Curation">003E87</idno><idno type="wicri:Area/Hal/Checkpoint">002916</idno><idno type="wicri:explorRef" wicri:stream="Hal" wicri:step="Checkpoint">002916</idno><idno type="wicri:Area/Main/Merge">003372</idno><idno type="wicri:Area/Main/Curation">003292</idno><idno type="wicri:Area/Main/Exploration">003292</idno></publicationStmt><sourceDesc><biblStruct><analytic><title xml:lang="en">Quasipolynomial Normalisation in Deep Inference via Atomic Flows and Threshold Formulae</title><author><name sortKey="Bruscoli, Paola" sort="Bruscoli, Paola" uniqKey="Bruscoli P" first="Paola" last="Bruscoli">Paola Bruscoli</name><affiliation wicri:level="1"><hal:affiliation type="researchteam" xml:id="struct-2347" status="OLD"><idno type="RNSR">199618306V</idno><orgName>Linear logic, proof networks and categorial grammars</orgName><orgName type="acronym">CALLIGRAMME</orgName><desc><address><country key="FR"></country></address><ref type="url">http://www.inria.fr/equipes/calligramme</ref></desc><listRelation><relation active="#struct-160" type="direct"></relation><relation name="UMR7503" active="#struct-441569" type="indirect"></relation><relation active="#struct-300009" type="indirect"></relation><relation active="#struct-300291" type="indirect"></relation><relation active="#struct-300292" type="indirect"></relation><relation active="#struct-300293" type="indirect"></relation><relation active="#struct-2496" type="direct"></relation></listRelation><tutelles><tutelle active="#struct-160" type="direct"><org type="laboratory" xml:id="struct-160" status="OLD"><orgName>Laboratoire Lorrain de Recherche en Informatique et ses Applications</orgName><orgName type="acronym">LORIA</orgName><desc><address><addrLine>Campus Scientifique BP 239 54506 Vandoeuvre-lès-Nancy Cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.loria.fr</ref></desc><listRelation><relation name="UMR7503" active="#struct-441569" type="direct"></relation><relation active="#struct-300009" type="direct"></relation><relation active="#struct-300291" type="direct"></relation><relation active="#struct-300292" type="direct"></relation><relation active="#struct-300293" type="direct"></relation></listRelation></org></tutelle><tutelle name="UMR7503" active="#struct-441569" type="indirect"><org type="institution" xml:id="struct-441569" status="VALID"><idno type="ISNI">0000000122597504</idno><idno type="IdRef">02636817X</idno><orgName>Centre National de la Recherche Scientifique</orgName><orgName type="acronym">CNRS</orgName><date type="start">1939-10-19</date><desc><address><country key="FR"></country></address><ref type="url">http://www.cnrs.fr/</ref></desc></org></tutelle><tutelle active="#struct-300009" type="indirect"><org type="institution" xml:id="struct-300009" status="VALID"><orgName>Institut National de Recherche en Informatique et en Automatique</orgName><orgName type="acronym">Inria</orgName><desc><address><addrLine>Domaine de VoluceauRocquencourt - BP 10578153 Le Chesnay Cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.inria.fr/en/</ref></desc></org></tutelle><tutelle active="#struct-300291" type="indirect"><org type="institution" xml:id="struct-300291" status="OLD"><orgName>Université Henri Poincaré - Nancy 1</orgName><orgName type="acronym">UHP</orgName><date type="end">2011-12-31</date><desc><address><addrLine>24-30 rue Lionnois, BP 60120, 54 003 NANCY cedex, France</addrLine><country key="FR"></country></address></desc></org></tutelle><tutelle active="#struct-300292" type="indirect"><org type="institution" xml:id="struct-300292" status="OLD"><orgName>Université Nancy 2</orgName><date type="end">2011-12-31</date><desc><address><addrLine>91 avenue de la Libération, BP 454, 54001 Nancy cedex</addrLine><country key="FR"></country></address></desc></org></tutelle><tutelle active="#struct-300293" type="indirect"><org type="institution" xml:id="struct-300293" status="OLD"><orgName>Institut National Polytechnique de Lorraine</orgName><orgName type="acronym">INPL</orgName><date type="end">2011-12-31</date><desc><address><country key="FR"></country></address></desc></org></tutelle><tutelle active="#struct-2496" type="direct"><org type="laboratory" xml:id="struct-2496" status="OLD"><orgName>INRIA Lorraine</orgName><desc><address><addrLine>615 rue du Jardin Botanique 54600 Villers-lès-Nancy</addrLine><country key="FR"></country></address><ref type="url">http://www.inria.fr/centre-de-recherche-inria/nancy-grand-est</ref></desc><listRelation><relation active="#struct-300009" type="direct"></relation></listRelation></org></tutelle></tutelles></hal:affiliation><country>France</country><placeName><settlement type="city">Nancy</settlement><region type="region" nuts="2">Grand Est</region><region type="old region" nuts="2">Lorraine (région)</region></placeName><orgName type="university">Université Nancy 2</orgName><orgName type="institution" wicri:auto="newGroup">Université de Lorraine</orgName><placeName><settlement type="city">Nancy</settlement><region type="region" nuts="2">Grand Est</region><region type="old region" nuts="2">Lorraine (région)</region></placeName><orgName type="university">Institut national polytechnique de Lorraine</orgName><orgName type="institution" wicri:auto="newGroup">Université de Lorraine</orgName></affiliation></author><author><name sortKey="Guglielmi, Alessio" sort="Guglielmi, Alessio" uniqKey="Guglielmi A" first="Alessio" last="Guglielmi">Alessio Guglielmi</name><affiliation wicri:level="1"><hal:affiliation type="researchteam" xml:id="struct-2347" status="OLD"><idno type="RNSR">199618306V</idno><orgName>Linear logic, proof networks and categorial grammars</orgName><orgName type="acronym">CALLIGRAMME</orgName><desc><address><country key="FR"></country></address><ref type="url">http://www.inria.fr/equipes/calligramme</ref></desc><listRelation><relation active="#struct-160" type="direct"></relation><relation name="UMR7503" active="#struct-441569" type="indirect"></relation><relation active="#struct-300009" type="indirect"></relation><relation active="#struct-300291" type="indirect"></relation><relation active="#struct-300292" type="indirect"></relation><relation active="#struct-300293" type="indirect"></relation><relation active="#struct-2496" type="direct"></relation></listRelation><tutelles><tutelle active="#struct-160" type="direct"><org type="laboratory" xml:id="struct-160" status="OLD"><orgName>Laboratoire Lorrain de Recherche en Informatique et ses Applications</orgName><orgName type="acronym">LORIA</orgName><desc><address><addrLine>Campus Scientifique BP 239 54506 Vandoeuvre-lès-Nancy Cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.loria.fr</ref></desc><listRelation><relation name="UMR7503" active="#struct-441569" type="direct"></relation><relation active="#struct-300009" type="direct"></relation><relation active="#struct-300291" type="direct"></relation><relation active="#struct-300292" type="direct"></relation><relation active="#struct-300293" type="direct"></relation></listRelation></org></tutelle><tutelle name="UMR7503" active="#struct-441569" type="indirect"><org type="institution" xml:id="struct-441569" status="VALID"><idno type="ISNI">0000000122597504</idno><idno type="IdRef">02636817X</idno><orgName>Centre National de la Recherche Scientifique</orgName><orgName type="acronym">CNRS</orgName><date type="start">1939-10-19</date><desc><address><country key="FR"></country></address><ref type="url">http://www.cnrs.fr/</ref></desc></org></tutelle><tutelle active="#struct-300009" type="indirect"><org type="institution" xml:id="struct-300009" status="VALID"><orgName>Institut National de Recherche en Informatique et en Automatique</orgName><orgName type="acronym">Inria</orgName><desc><address><addrLine>Domaine de VoluceauRocquencourt - BP 10578153 Le Chesnay Cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.inria.fr/en/</ref></desc></org></tutelle><tutelle active="#struct-300291" type="indirect"><org type="institution" xml:id="struct-300291" status="OLD"><orgName>Université Henri Poincaré - Nancy 1</orgName><orgName type="acronym">UHP</orgName><date type="end">2011-12-31</date><desc><address><addrLine>24-30 rue Lionnois, BP 60120, 54 003 NANCY cedex, France</addrLine><country key="FR"></country></address></desc></org></tutelle><tutelle active="#struct-300292" type="indirect"><org type="institution" xml:id="struct-300292" status="OLD"><orgName>Université Nancy 2</orgName><date type="end">2011-12-31</date><desc><address><addrLine>91 avenue de la Libération, BP 454, 54001 Nancy cedex</addrLine><country key="FR"></country></address></desc></org></tutelle><tutelle active="#struct-300293" type="indirect"><org type="institution" xml:id="struct-300293" status="OLD"><orgName>Institut National Polytechnique de Lorraine</orgName><orgName type="acronym">INPL</orgName><date type="end">2011-12-31</date><desc><address><country key="FR"></country></address></desc></org></tutelle><tutelle active="#struct-2496" type="direct"><org type="laboratory" xml:id="struct-2496" status="OLD"><orgName>INRIA Lorraine</orgName><desc><address><addrLine>615 rue du Jardin Botanique 54600 Villers-lès-Nancy</addrLine><country key="FR"></country></address><ref type="url">http://www.inria.fr/centre-de-recherche-inria/nancy-grand-est</ref></desc><listRelation><relation active="#struct-300009" type="direct"></relation></listRelation></org></tutelle></tutelles></hal:affiliation><country>France</country><placeName><settlement type="city">Nancy</settlement><region type="region" nuts="2">Grand Est</region><region type="old region" nuts="2">Lorraine (région)</region></placeName><orgName type="university">Université Nancy 2</orgName><orgName type="institution" wicri:auto="newGroup">Université de Lorraine</orgName><placeName><settlement type="city">Nancy</settlement><region type="region" nuts="2">Grand Est</region><region type="old region" nuts="2">Lorraine (région)</region></placeName><orgName type="university">Institut national polytechnique de Lorraine</orgName><orgName type="institution" wicri:auto="newGroup">Université de Lorraine</orgName></affiliation></author><author><name sortKey="Gundersen, Tom" sort="Gundersen, Tom" uniqKey="Gundersen T" first="Tom" last="Gundersen">Tom Gundersen</name><affiliation wicri:level="1"><hal:affiliation type="laboratory" xml:id="struct-2071" status="VALID"><orgName>Laboratoire d'informatique de l'École polytechnique [Palaiseau]</orgName><orgName type="acronym">LIX</orgName><desc><address><addrLine>Route de Saclay 91128 PALAISEAU CEDEX</addrLine><country key="FR"></country></address><ref type="url">http://www.lix.polytechnique.fr/</ref></desc><listRelation><relation active="#struct-300340" type="direct"></relation><relation name="UMR7161" active="#struct-441569" type="direct"></relation></listRelation><tutelles><tutelle active="#struct-300340" type="direct"><org type="institution" xml:id="struct-300340" status="VALID"><orgName>Polytechnique - X</orgName><desc><address><country key="FR"></country></address></desc></org></tutelle><tutelle name="UMR7161" active="#struct-441569" type="direct"><org type="institution" xml:id="struct-441569" status="VALID"><idno type="ISNI">0000000122597504</idno><idno type="IdRef">02636817X</idno><orgName>Centre National de la Recherche Scientifique</orgName><orgName type="acronym">CNRS</orgName><date type="start">1939-10-19</date><desc><address><country key="FR"></country></address><ref type="url">http://www.cnrs.fr/</ref></desc></org></tutelle></tutelles></hal:affiliation><country>France</country></affiliation></author><author><name sortKey="Parigot, Michel" sort="Parigot, Michel" uniqKey="Parigot M" first="Michel" last="Parigot">Michel Parigot</name><affiliation wicri:level="1"><hal:affiliation type="laboratory" xml:id="struct-1067" status="OLD"><orgName>Preuves, Programmes et Systèmes</orgName><orgName type="acronym">PPS</orgName><date type="end">2015-12-31</date><desc><address><addrLine>Université Paris Diderot, Bât. Sophie Germain, case postale 7014, 75205 Paris Cedex 13</addrLine><country key="FR"></country></address><ref type="url">http://www.pps.univ-paris-diderot.fr</ref></desc><listRelation><relation active="#struct-300301" type="direct"></relation><relation name="UMR7126" active="#struct-441569" type="direct"></relation></listRelation><tutelles><tutelle active="#struct-300301" type="direct"><org type="institution" xml:id="struct-300301" status="VALID"><orgName>Université Paris Diderot - Paris 7</orgName><orgName type="acronym">UP7</orgName><desc><address><addrLine>5 rue Thomas-Mann - 75205 Paris cedex 13</addrLine><country key="FR"></country></address><ref type="url">http://www.univ-paris-diderot.fr</ref></desc></org></tutelle><tutelle name="UMR7126" active="#struct-441569" type="direct"><org type="institution" xml:id="struct-441569" status="VALID"><idno type="ISNI">0000000122597504</idno><idno type="IdRef">02636817X</idno><orgName>Centre National de la Recherche Scientifique</orgName><orgName type="acronym">CNRS</orgName><date type="start">1939-10-19</date><desc><address><country key="FR"></country></address><ref type="url">http://www.cnrs.fr/</ref></desc></org></tutelle></tutelles></hal:affiliation><country>France</country></affiliation></author></analytic></biblStruct></sourceDesc></fileDesc><profileDesc><textClass></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">Jerábek showed that analytic propositional-logic deep-inference proofs can be constructed in quasipolynomial time from nonanalytic proofs. In this work, we improve on that as follows: 1) we significantly simplify the technique; 2) our normalisation procedure is direct, i.e., it is internal to deep inference. The paper is self-contained, and provides a starting point and a good deal of information for tackling the problem of whether a polynomial-time normalisation procedure exists.</div></front></TEI><affiliations><list><country><li>France</li></country><region><li>Grand Est</li><li>Lorraine (région)</li></region><settlement><li>Nancy</li></settlement><orgName><li>Institut national polytechnique de Lorraine</li><li>Université Nancy 2</li><li>Université de Lorraine</li></orgName></list><tree><country name="France"><region name="Grand Est"><name sortKey="Bruscoli, Paola" sort="Bruscoli, Paola" uniqKey="Bruscoli P" first="Paola" last="Bruscoli">Paola Bruscoli</name></region><name sortKey="Guglielmi, Alessio" sort="Guglielmi, Alessio" uniqKey="Guglielmi A" first="Alessio" last="Guglielmi">Alessio Guglielmi</name><name sortKey="Gundersen, Tom" sort="Gundersen, Tom" uniqKey="Gundersen T" first="Tom" last="Gundersen">Tom Gundersen</name><name sortKey="Parigot, Michel" sort="Parigot, Michel" uniqKey="Parigot M" first="Michel" last="Parigot">Michel Parigot</name></country></tree></affiliations></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Exploration
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 003292 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 003292 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Main
|étape= Exploration
|type= RBID
|clé= Hal:inria-00441213
|texte= Quasipolynomial Normalisation in Deep Inference via Atomic Flows and Threshold Formulae
}}
| This area was generated with Dilib version V0.6.33. |  |