InforLorV4, Main, Merge, bibRecord, 00A611

Efficient resource management for linear logic proof search

Identifieur interne : 00A611 ( Main/Merge ); précédent : 00A610; suivant : 00A612

Efficient resource management for linear logic proof search

Auteurs : I. Cervesato [États-Unis] ; J. S. Hodas [États-Unis] ; F. Pfenning [États-Unis]

Source :

Theoretical computer science [ 0304-3975 ] ; 2000.

RBID : Pascal:00-0103550

Descripteurs français

Pascal (Inist)
- Logique, Programmation logique, Démonstration théorème, Sémantique opérationnelle, Gestion ressource, Contexte, Calcul résolution, Recherche preuve, Logique linéaire, Formule Harrop.

English descriptors

KwdEn :
- Context, Harrop formula, Linear logic, Logic, Logical programming, Operational semantics, Proof search, Resolution calculus, Resource management, Theorem proving.

Abstract

The design of linear logic programming languages and theorem provers opens a number of new implementation challenges not present in more traditional logic languages such as Horn clauses (Prolog) and hereditary Harrop formulas (λProlog and Elf). Among these, the problem of efficiently managing the linear context when solving a goal is of crucial importance for the use of these systems in non-trivial applications. This paper studies this problem in the case of Lolli [10], though its results have application to other systems including those based on linear type theory. We first give a proof-theoretic presentation of the operational semantics of this language as a resolution calculus. We then present a series of resource management systems designed to eliminate the non-determinism in the distribution of linear formulas that undermines the efficiency of a direct implementation of this system.

Links toward previous steps (curation, corpus...)

to stream PascalFrancis, to step Corpus: 000A68
to stream PascalFrancis, to step Curation: 000014
to stream PascalFrancis, to step Checkpoint: 000A05

Links to Exploration step

Pascal:00-0103550

Le document en format XML

<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en" level="a">Efficient resource management for linear logic proof search</title>
<author><name sortKey="Cervesato, I" sort="Cervesato, I" uniqKey="Cervesato I" first="I." last="Cervesato">I. Cervesato</name>
<affiliation wicri:level="1"><inist:fA14 i1="01"><s1>Department of Computer Science, Stanford University</s1>
<s2>Stanford, CA 94305-9045</s2>
<s3>USA</s3>
<sZ>1 aut.</sZ>
</inist:fA14>
<country>États-Unis</country>
<wicri:noRegion>Stanford, CA 94305-9045</wicri:noRegion>
</affiliation>
</author>
<author><name sortKey="Hodas, J S" sort="Hodas, J S" uniqKey="Hodas J" first="J. S." last="Hodas">J. S. Hodas</name>
<affiliation wicri:level="1"><inist:fA14 i1="02"><s1>Computer Science Department, Harvey Mudd College</s1>
<s2>Claremont, CA 91711</s2>
<s3>USA</s3>
<sZ>2 aut.</sZ>
</inist:fA14>
<country>États-Unis</country>
<wicri:noRegion>Claremont, CA 91711</wicri:noRegion>
</affiliation>
</author>
<author><name sortKey="Pfenning, F" sort="Pfenning, F" uniqKey="Pfenning F" first="F." last="Pfenning">F. Pfenning</name>
<affiliation wicri:level="4"><inist:fA14 i1="03"><s1>Department of Computer Science, Carnegie Mellon University</s1>
<s2>Pittsburgh, PA 15213-3891</s2>
<s3>USA</s3>
<sZ>3 aut.</sZ>
</inist:fA14>
<country>États-Unis</country>
<placeName><settlement type="city">Pittsburgh</settlement>
<region type="state">Pennsylvanie</region>
</placeName>
<orgName type="university">Université Carnegie-Mellon</orgName>
</affiliation>
</author>
</titleStmt>
<publicationStmt><idno type="wicri:source">INIST</idno>
<idno type="inist">00-0103550</idno>
<date when="2000">2000</date>
<idno type="stanalyst">PASCAL 00-0103550 INIST</idno>
<idno type="RBID">Pascal:00-0103550</idno>
<idno type="wicri:Area/PascalFrancis/Corpus">000A68</idno>
<idno type="wicri:Area/PascalFrancis/Curation">000014</idno>
<idno type="wicri:Area/PascalFrancis/Checkpoint">000A05</idno>
<idno type="wicri:explorRef" wicri:stream="PascalFrancis" wicri:step="Checkpoint">000A05</idno>
<idno type="wicri:doubleKey">0304-3975:2000:Cervesato I:efficient:resource:management</idno>
<idno type="wicri:Area/Main/Merge">00A611</idno>
</publicationStmt>
<sourceDesc><biblStruct><analytic><title xml:lang="en" level="a">Efficient resource management for linear logic proof search</title>
<author><name sortKey="Cervesato, I" sort="Cervesato, I" uniqKey="Cervesato I" first="I." last="Cervesato">I. Cervesato</name>
<affiliation wicri:level="1"><inist:fA14 i1="01"><s1>Department of Computer Science, Stanford University</s1>
<s2>Stanford, CA 94305-9045</s2>
<s3>USA</s3>
<sZ>1 aut.</sZ>
</inist:fA14>
<country>États-Unis</country>
<wicri:noRegion>Stanford, CA 94305-9045</wicri:noRegion>
</affiliation>
</author>
<author><name sortKey="Hodas, J S" sort="Hodas, J S" uniqKey="Hodas J" first="J. S." last="Hodas">J. S. Hodas</name>
<affiliation wicri:level="1"><inist:fA14 i1="02"><s1>Computer Science Department, Harvey Mudd College</s1>
<s2>Claremont, CA 91711</s2>
<s3>USA</s3>
<sZ>2 aut.</sZ>
</inist:fA14>
<country>États-Unis</country>
<wicri:noRegion>Claremont, CA 91711</wicri:noRegion>
</affiliation>
</author>
<author><name sortKey="Pfenning, F" sort="Pfenning, F" uniqKey="Pfenning F" first="F." last="Pfenning">F. Pfenning</name>
<affiliation wicri:level="4"><inist:fA14 i1="03"><s1>Department of Computer Science, Carnegie Mellon University</s1>
<s2>Pittsburgh, PA 15213-3891</s2>
<s3>USA</s3>
<sZ>3 aut.</sZ>
</inist:fA14>
<country>États-Unis</country>
<placeName><settlement type="city">Pittsburgh</settlement>
<region type="state">Pennsylvanie</region>
</placeName>
<orgName type="university">Université Carnegie-Mellon</orgName>
</affiliation>
</author>
</analytic>
<series><title level="j" type="main">Theoretical computer science</title>
<title level="j" type="abbreviated">Theor. comput. sci.</title>
<idno type="ISSN">0304-3975</idno>
<imprint><date when="2000">2000</date>
</imprint>
</series>
</biblStruct>
</sourceDesc>
<seriesStmt><title level="j" type="main">Theoretical computer science</title>
<title level="j" type="abbreviated">Theor. comput. sci.</title>
<idno type="ISSN">0304-3975</idno>
</seriesStmt>
</fileDesc>
<profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>Context</term>
<term>Harrop formula</term>
<term>Linear logic</term>
<term>Logic</term>
<term>Logical programming</term>
<term>Operational semantics</term>
<term>Proof search</term>
<term>Resolution calculus</term>
<term>Resource management</term>
<term>Theorem proving</term>
</keywords>
<keywords scheme="Pascal" xml:lang="fr"><term>Logique</term>
<term>Programmation logique</term>
<term>Démonstration théorème</term>
<term>Sémantique opérationnelle</term>
<term>Gestion ressource</term>
<term>Contexte</term>
<term>Calcul résolution</term>
<term>Recherche preuve</term>
<term>Logique linéaire</term>
<term>Formule Harrop</term>
</keywords>
</textClass>
</profileDesc>
</teiHeader>
<front><div type="abstract" xml:lang="en">The design of linear logic programming languages and theorem provers opens a number of new implementation challenges not present in more traditional logic languages such as Horn clauses (Prolog) and hereditary Harrop formulas (λProlog and Elf). Among these, the problem of efficiently managing the linear context when solving a goal is of crucial importance for the use of these systems in non-trivial applications. This paper studies this problem in the case of Lolli [10], though its results have application to other systems including those based on linear type theory. We first give a proof-theoretic presentation of the operational semantics of this language as a resolution calculus. We then present a series of resource management systems designed to eliminate the non-determinism in the distribution of linear formulas that undermines the efficiency of a direct implementation of this system.</div>
</front>
</TEI>
<affiliations><list><country><li>États-Unis</li>
</country>
<region><li>Pennsylvanie</li>
</region>
<settlement><li>Pittsburgh</li>
</settlement>
<orgName><li>Université Carnegie-Mellon</li>
</orgName>
</list>
<tree><country name="États-Unis"><noRegion><name sortKey="Cervesato, I" sort="Cervesato, I" uniqKey="Cervesato I" first="I." last="Cervesato">I. Cervesato</name>
</noRegion>
<name sortKey="Hodas, J S" sort="Hodas, J S" uniqKey="Hodas J" first="J. S." last="Hodas">J. S. Hodas</name>
<name sortKey="Pfenning, F" sort="Pfenning, F" uniqKey="Pfenning F" first="F." last="Pfenning">F. Pfenning</name>
</country>
</tree>
</affiliations>
</record>

Pour manipuler ce document sous Unix (Dilib)

EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Merge

HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 00A611 | SxmlIndent | more

HfdSelect -h $EXPLOR_AREA/Data/Main/Merge/biblio.hfd -nk 00A611 | SxmlIndent | more

Pour mettre un lien sur cette page dans le réseau Wicri

{{Explor lien
   |wiki=    Wicri/Lorraine
   |area=    InforLorV4
   |flux=    Main
   |étape=   Merge
   |type=    RBID
   |clé=     Pascal:00-0103550
   |texte=   Efficient resource management for linear logic proof search
}}

This area was generated with Dilib version V0.6.33.
Data generation: Mon Jun 10 21:56:28 2019. Site generation: Fri Feb 25 15:29:27 2022

	Serveur d'exploration sur la recherche en informatique en Lorraine
	Attention, ce site est en cours de développement ! Attention, site généré par des moyens informatiques à partir de corpus bruts. Les informations ne sont donc pas validées.

Serveur d'exploration sur la recherche en informatique en Lorraine

Efficient resource management for linear logic proof search

Efficient resource management for linear logic proof search

Source :

Descripteurs français

English descriptors

Abstract

Links toward previous steps (curation, corpus...)

Links to Exploration step

Le document en format XML

Pour manipuler ce document sous Unix (Dilib)

Pour mettre un lien sur cette page dans le réseau Wicri