A PSPACE-complete fragment of second-order linear logic
Identifieur interne : 002016 ( Istex/Curation ); précédent : 002015; suivant : 002017A PSPACE-complete fragment of second-order linear logic
Auteurs : G. Perrier [France]Source :
- Theoretical Computer Science [ 0304-3975 ] ; 1999.
English descriptors
- Teeft :
- Active subgoal, Active subgoals, Calculus, Chaining, Computer science, Current goal, Decision procedure, Decomposed, Deduction, Deduction procedure, Deduction procedures, Deduction step, Emms, Existentially, Finite number, First problem, First step, Fresh variables, Imall, Induction hypothesis, Inference permutability, Initial goal, Initial sequent, Instantiated, Instantiation, Intuitionistic, Last goal, Linear logic, Main formula, Mall2, Mall2 formula, Multiplicative, Multiplicative fragment, Negative occurrences, Negative translation, Normal proofs, Perrier, Premiss, Proof search, Propositional, Provable, Provable sequent, Same time, Second order, Sequent, Sequent calculus, Sequents, Side condition, Subformula, Subgoal, Subgoals, Successful deduction, Theoretical computer science, Undecidability, Unique subgoal, Unknown formula.
Abstract
Abstract: Existentially quantified variables are the source of non-decidability for second-order linear logic without exponentials (MALL2). We present a decision procedure for a fragment of MALL2 based on a canonical instantiation of these variables and using inference permutability in proofs. We also establish that this fragment is PSPACE-complete.
Url:
DOI: 10.1016/S0304-3975(98)00315-6
Links toward previous steps (curation, corpus...)
- to stream Istex, to step Corpus: Pour aller vers cette notice dans l'étape Curation :002042
Links to Exploration step
ISTEX:8C05ACF2B2B56A560FAD0FF45E52A521EC648D3DLe document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title>A PSPACE-complete fragment of second-order linear logic</title><author><name sortKey="Perrier, G" sort="Perrier, G" uniqKey="Perrier G" first="G." last="Perrier">G. Perrier</name><affiliation wicri:level="1"><mods:affiliation>LORIA — Université Nancy 2, Campus Scientifique-B.P. 239, 54506 Vandœuvre-les-Nancy Cedex, France</mods:affiliation><country xml:lang="fr">France</country><wicri:regionArea>LORIA — Université Nancy 2, Campus Scientifique-B.P. 239, 54506 Vandœuvre-les-Nancy Cedex</wicri:regionArea></affiliation><affiliation wicri:level="1"><mods:affiliation>E-mail: perrier@loria.fr</mods:affiliation><country wicri:rule="url">France</country></affiliation></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:8C05ACF2B2B56A560FAD0FF45E52A521EC648D3D</idno><date when="1999" year="1999">1999</date><idno type="doi">10.1016/S0304-3975(98)00315-6</idno><idno type="url">https://api.istex.fr/ark:/67375/6H6-JGNF9TVZ-2/fulltext.pdf</idno><idno type="wicri:Area/Istex/Corpus">002042</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">002042</idno><idno type="wicri:Area/Istex/Curation">002016</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a">A PSPACE-complete fragment of second-order linear logic</title><author><name sortKey="Perrier, G" sort="Perrier, G" uniqKey="Perrier G" first="G." last="Perrier">G. Perrier</name><affiliation wicri:level="1"><mods:affiliation>LORIA — Université Nancy 2, Campus Scientifique-B.P. 239, 54506 Vandœuvre-les-Nancy Cedex, France</mods:affiliation><country xml:lang="fr">France</country><wicri:regionArea>LORIA — Université Nancy 2, Campus Scientifique-B.P. 239, 54506 Vandœuvre-les-Nancy Cedex</wicri:regionArea></affiliation><affiliation wicri:level="1"><mods:affiliation>E-mail: perrier@loria.fr</mods:affiliation><country wicri:rule="url">France</country></affiliation></author></analytic><monogr></monogr><series><title level="j">Theoretical Computer Science</title><title level="j" type="abbrev">TCS</title><idno type="ISSN">0304-3975</idno><imprint><publisher>ELSEVIER</publisher><date type="published" when="1999">1999</date><biblScope unit="volume">224</biblScope><biblScope unit="issue">1–2</biblScope><biblScope unit="page" from="267">267</biblScope><biblScope unit="page" to="289">289</biblScope></imprint><idno type="ISSN">0304-3975</idno></series></biblStruct></sourceDesc><seriesStmt><idno type="ISSN">0304-3975</idno></seriesStmt></fileDesc><profileDesc><textClass><keywords scheme="Teeft" xml:lang="en"><term>Active subgoal</term><term>Active subgoals</term><term>Calculus</term><term>Chaining</term><term>Computer science</term><term>Current goal</term><term>Decision procedure</term><term>Decomposed</term><term>Deduction</term><term>Deduction procedure</term><term>Deduction procedures</term><term>Deduction step</term><term>Emms</term><term>Existentially</term><term>Finite number</term><term>First problem</term><term>First step</term><term>Fresh variables</term><term>Imall</term><term>Induction hypothesis</term><term>Inference permutability</term><term>Initial goal</term><term>Initial sequent</term><term>Instantiated</term><term>Instantiation</term><term>Intuitionistic</term><term>Last goal</term><term>Linear logic</term><term>Main formula</term><term>Mall2</term><term>Mall2 formula</term><term>Multiplicative</term><term>Multiplicative fragment</term><term>Negative occurrences</term><term>Negative translation</term><term>Normal proofs</term><term>Perrier</term><term>Premiss</term><term>Proof search</term><term>Propositional</term><term>Provable</term><term>Provable sequent</term><term>Same time</term><term>Second order</term><term>Sequent</term><term>Sequent calculus</term><term>Sequents</term><term>Side condition</term><term>Subformula</term><term>Subgoal</term><term>Subgoals</term><term>Successful deduction</term><term>Theoretical computer science</term><term>Undecidability</term><term>Unique subgoal</term><term>Unknown formula</term></keywords></textClass><langUsage><language ident="en">en</language></langUsage></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">Abstract: Existentially quantified variables are the source of non-decidability for second-order linear logic without exponentials (MALL2). We present a decision procedure for a fragment of MALL2 based on a canonical instantiation of these variables and using inference permutability in proofs. We also establish that this fragment is PSPACE-complete.</div></front></TEI></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Istex/Curation
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 002016 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Istex/Curation/biblio.hfd -nk 002016 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Istex
|étape= Curation
|type= RBID
|clé= ISTEX:8C05ACF2B2B56A560FAD0FF45E52A521EC648D3D
|texte= A PSPACE-complete fragment of second-order linear logic
}}
| This area was generated with Dilib version V0.6.33. |  |