A class of confluent term rewriting systems and unification
Identifieur interne : 001823 ( Istex/Curation ); précédent : 001822; suivant : 001824A class of confluent term rewriting systems and unification
Auteurs : Jia-Huai You [Canada] ; P. A. Subrahmanyam [États-Unis]Source :
- Journal of Automated Reasoning [ 0168-7433 ] ; 1986-12-01.
English descriptors
- KwdEn :
- Teeft :
- Algorithm, Canonical, Canonical term, Closure, Closure property, Complete algorithm, Complete sets, Complete unification algorithm, Completeness proof, Computer science, Confluence, Confluence property, Confluent, Confluent term, Equational, Equational programs, Equational theories, Equational theory, Equivalence classes, First occurrence, Function symbol, Functional programs, Input terms, Lefthand, Lefthand side, Linear term, Logic programming, Major transformation step, Minimum unifier, Normal form, Other hand, Proc, Reducible subterm, Reduction sequence, Reduction sequences, Residue, Righthand side, Second clause, Subrahmanyam, Substitution, Subterm, Subterms, Such equivalence classes, Theorem prover, Transformation process, Unification, Unifier.
Abstract
Abstract: The narrowing mechanism and term rewriting systems are powerful tools for constructing complete and efficient unification algorithms for useful classes of equational theories. This has been shown for the case where term rewriting systems are confluent and noetherian (i.e., terminating). In this paper we show that the narrowing mechanism, combined with ordinary unification, yields a complete unification algorithm for equational theories that can be described by a closed linear term rewriting system with the non-repetition property; this class allows non-terminating rewrite systems. For some special forms of input terms, narrowing generates complete sets of E-unifiers without resorting to the non-repetition property. The key observation underlying the proof is that a reduction sequence in this class of term rewriting system can be transformed into one which possesses properties that enable a completeness proof.
Url:
DOI: 10.1007/BF00248250
Links toward previous steps (curation, corpus...)
- to stream Istex, to step Corpus: Pour aller vers cette notice dans l'étape Curation :001842
Links to Exploration step
ISTEX:68E6ED1447766E95E1441638585383807D736062Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">A class of confluent term rewriting systems and unification</title>
<author><name sortKey="You, Jia Huai" sort="You, Jia Huai" uniqKey="You J" first="Jia-Huai" last="You">Jia-Huai You</name>
<affiliation wicri:level="1"><mods:affiliation>Department of Computing Science, University of Alberta, T6G 2H1, Edmonton, Alberta, Canada</mods:affiliation>
<country xml:lang="fr">Canada</country>
<wicri:regionArea>Department of Computing Science, University of Alberta, T6G 2H1, Edmonton, Alberta</wicri:regionArea>
</affiliation>
</author>
<author><name sortKey="Subrahmanyam, P A" sort="Subrahmanyam, P A" uniqKey="Subrahmanyam P" first="P. A." last="Subrahmanyam">P. A. Subrahmanyam</name>
<affiliation wicri:level="1"><mods:affiliation>AT&T Bell Laboratories, 07733, Holmdel, NJ, USA</mods:affiliation>
<country xml:lang="fr">États-Unis</country>
<wicri:regionArea>AT&T Bell Laboratories, 07733, Holmdel, NJ</wicri:regionArea>
</affiliation>
</author>
</titleStmt>
<publicationStmt><idno type="wicri:source">ISTEX</idno>
<idno type="RBID">ISTEX:68E6ED1447766E95E1441638585383807D736062</idno>
<date when="1986" year="1986">1986</date>
<idno type="doi">10.1007/BF00248250</idno>
<idno type="url">https://api.istex.fr/ark:/67375/1BB-X2CQM9FX-P/fulltext.pdf</idno>
<idno type="wicri:Area/Istex/Corpus">001842</idno>
<idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">001842</idno>
<idno type="wicri:Area/Istex/Curation">001823</idno>
</publicationStmt>
<sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">A class of confluent term rewriting systems and unification</title>
<author><name sortKey="You, Jia Huai" sort="You, Jia Huai" uniqKey="You J" first="Jia-Huai" last="You">Jia-Huai You</name>
<affiliation wicri:level="1"><mods:affiliation>Department of Computing Science, University of Alberta, T6G 2H1, Edmonton, Alberta, Canada</mods:affiliation>
<country xml:lang="fr">Canada</country>
<wicri:regionArea>Department of Computing Science, University of Alberta, T6G 2H1, Edmonton, Alberta</wicri:regionArea>
</affiliation>
</author>
<author><name sortKey="Subrahmanyam, P A" sort="Subrahmanyam, P A" uniqKey="Subrahmanyam P" first="P. A." last="Subrahmanyam">P. A. Subrahmanyam</name>
<affiliation wicri:level="1"><mods:affiliation>AT&T Bell Laboratories, 07733, Holmdel, NJ, USA</mods:affiliation>
<country xml:lang="fr">États-Unis</country>
<wicri:regionArea>AT&T Bell Laboratories, 07733, Holmdel, NJ</wicri:regionArea>
</affiliation>
</author>
</analytic>
<monogr></monogr>
<series><title level="j">Journal of Automated Reasoning</title>
<title level="j" type="abbrev">Journal of Automated Reasoning</title>
<idno type="ISSN">0168-7433</idno>
<idno type="eISSN">1573-0670</idno>
<imprint><publisher>Kluwer Academic Publishers</publisher>
<pubPlace>Dordrecht</pubPlace>
<date type="published" when="1986-12-01">1986-12-01</date>
<biblScope unit="volume">2</biblScope>
<biblScope unit="issue">4</biblScope>
<biblScope unit="page" from="391">391</biblScope>
<biblScope unit="page" to="418">418</biblScope>
</imprint>
<idno type="ISSN">0168-7433</idno>
</series>
</biblStruct>
</sourceDesc>
<seriesStmt><idno type="ISSN">0168-7433</idno>
</seriesStmt>
</fileDesc>
<profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>E-unification</term>
<term>Term rewriting systems</term>
<term>equational theories</term>
<term>narrowing</term>
</keywords>
<keywords scheme="Teeft" xml:lang="en"><term>Algorithm</term>
<term>Canonical</term>
<term>Canonical term</term>
<term>Closure</term>
<term>Closure property</term>
<term>Complete algorithm</term>
<term>Complete sets</term>
<term>Complete unification algorithm</term>
<term>Completeness proof</term>
<term>Computer science</term>
<term>Confluence</term>
<term>Confluence property</term>
<term>Confluent</term>
<term>Confluent term</term>
<term>Equational</term>
<term>Equational programs</term>
<term>Equational theories</term>
<term>Equational theory</term>
<term>Equivalence classes</term>
<term>First occurrence</term>
<term>Function symbol</term>
<term>Functional programs</term>
<term>Input terms</term>
<term>Lefthand</term>
<term>Lefthand side</term>
<term>Linear term</term>
<term>Logic programming</term>
<term>Major transformation step</term>
<term>Minimum unifier</term>
<term>Normal form</term>
<term>Other hand</term>
<term>Proc</term>
<term>Reducible subterm</term>
<term>Reduction sequence</term>
<term>Reduction sequences</term>
<term>Residue</term>
<term>Righthand side</term>
<term>Second clause</term>
<term>Subrahmanyam</term>
<term>Substitution</term>
<term>Subterm</term>
<term>Subterms</term>
<term>Such equivalence classes</term>
<term>Theorem prover</term>
<term>Transformation process</term>
<term>Unification</term>
<term>Unifier</term>
</keywords>
</textClass>
<langUsage><language ident="en">en</language>
</langUsage>
</profileDesc>
</teiHeader>
<front><div type="abstract" xml:lang="en">Abstract: The narrowing mechanism and term rewriting systems are powerful tools for constructing complete and efficient unification algorithms for useful classes of equational theories. This has been shown for the case where term rewriting systems are confluent and noetherian (i.e., terminating). In this paper we show that the narrowing mechanism, combined with ordinary unification, yields a complete unification algorithm for equational theories that can be described by a closed linear term rewriting system with the non-repetition property; this class allows non-terminating rewrite systems. For some special forms of input terms, narrowing generates complete sets of E-unifiers without resorting to the non-repetition property. The key observation underlying the proof is that a reduction sequence in this class of term rewriting system can be transformed into one which possesses properties that enable a completeness proof.</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 001823 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Istex/Curation/biblio.hfd -nk 001823 | 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:68E6ED1447766E95E1441638585383807D736062 |texte= A class of confluent term rewriting systems and unification }}
This area was generated with Dilib version V0.6.33. |