On word problems in equational theories
Identifieur interne : 00E606 ( Main/Exploration ); précédent : 00E605; suivant : 00E607On word problems in equational theories
Auteurs : Jieh Hsiang [États-Unis] ; Michael Rusinowitch [France]Source :
- Lecture Notes in Computer Science [ 0302-9743 ]
Abstract
Abstract: The Knuth-Bendix procedure for word problems in universal algebra is known to be very effective when it is applicable. However, the procedure will fail if it generates equations which cannot be oriented into rules (i.e., the system is not noetherian), or if it generates infinitely many rules (i.e., the system is not confluent). In 1981 Huet showed that even if the system is not confluent, the Knuth-Bendix procedure still yields a semi-decision procedure for word problems, provided that every equation can be oriented. In this paper we show that even if some equations are not orientable, the Knuth-Bendix procedure can still be modified into a reasonably efficient semi-decision procedure for word problems in equational theories. Thus, we have lifted the noetherian requirement in the Knuth-Bendix procedure. Several confluence results, extensions, and experiments are given. So are some comparisons with related work. The proof of completeness, which is an interesting subject by itself, employs a new proof technique which utilizes a notion of transfinite semantic trees designed for proving refutational completeness of theorem proving methods in general. The outline of the paper is as follows: Section 1 briefly introduces term rewriting. The unfailing Knuth-Bendix procedure and confluence results are given in Section 2, together with some discussions and comparisons. Section 3 extends the results to a more general theory which includes inequalities. Simplification strategies are given in Section 4. In Section 5 we present the completeness proofs, as well as a framework of theorem proving strategies which captures the deletion strategies and fairness of search plans. Section 6 describes an implementation with some experimental results. Section contains some comparisons and discussions. Research reported in this paper is supported in part by the NSF grant DCS-8401624 and the Greco de Programmation of France.
Url:
DOI: 10.1007/3-540-18088-5_6
Affiliations:
Links toward previous steps (curation, corpus...)
- to stream Istex, to step Corpus: 002216
- to stream Istex, to step Curation: 002186
- to stream Istex, to step Checkpoint: 003535
- to stream Main, to step Merge: 00EE93
- to stream Main, to step Curation: 00E606
Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">On word problems in equational theories</title><author><name sortKey="Hsiang, Jieh" sort="Hsiang, Jieh" uniqKey="Hsiang J" first="Jieh" last="Hsiang">Jieh Hsiang</name></author><author><name sortKey="Rusinowitch, Michael" sort="Rusinowitch, Michael" uniqKey="Rusinowitch M" first="Michael" last="Rusinowitch">Michael Rusinowitch</name></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:92B2614133F8484DD858A5615D802B1CE3E0BD8D</idno><date when="1987" year="1987">1987</date><idno type="doi">10.1007/3-540-18088-5_6</idno><idno type="url">https://api.istex.fr/ark:/67375/HCB-CCV498Q2-R/fulltext.pdf</idno><idno type="wicri:Area/Istex/Corpus">002216</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">002216</idno><idno type="wicri:Area/Istex/Curation">002186</idno><idno type="wicri:Area/Istex/Checkpoint">003535</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Checkpoint">003535</idno><idno type="wicri:doubleKey">0302-9743:1987:Hsiang J:on:word:problems</idno><idno type="wicri:Area/Main/Merge">00EE93</idno><idno type="wicri:Area/Main/Curation">00E606</idno><idno type="wicri:Area/Main/Exploration">00E606</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">On word problems in equational theories</title><author><name sortKey="Hsiang, Jieh" sort="Hsiang, Jieh" uniqKey="Hsiang J" first="Jieh" last="Hsiang">Jieh Hsiang</name><affiliation wicri:level="2"><country xml:lang="fr">États-Unis</country><wicri:regionArea>Department of Computer Science, SUNY at Stony Brook, 11794, Stony Brook, NY</wicri:regionArea><placeName><region type="state">État de New York</region></placeName></affiliation></author><author><name sortKey="Rusinowitch, Michael" sort="Rusinowitch, Michael" uniqKey="Rusinowitch M" first="Michael" last="Rusinowitch">Michael Rusinowitch</name><affiliation wicri:level="3"><country xml:lang="fr">France</country><wicri:regionArea>CRIN, B.P. 239, 54506, Vandoeuvre-les-Nancy</wicri:regionArea><placeName><region type="region" nuts="2">Grand Est</region><region type="old region" nuts="2">Lorraine (région)</region><settlement type="city">Vandœuvre-lès-Nancy</settlement></placeName></affiliation></author></analytic><monogr></monogr><series><title level="s" type="main" xml:lang="en">Lecture Notes in Computer Science</title><title level="s" type="abbrev">Lect Notes Comput Sci</title><idno type="ISSN">0302-9743</idno><idno type="eISSN">1611-3349</idno><idno type="ISSN">0302-9743</idno></series></biblStruct></sourceDesc><seriesStmt><idno type="ISSN">0302-9743</idno></seriesStmt></fileDesc><profileDesc><textClass></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">Abstract: The Knuth-Bendix procedure for word problems in universal algebra is known to be very effective when it is applicable. However, the procedure will fail if it generates equations which cannot be oriented into rules (i.e., the system is not noetherian), or if it generates infinitely many rules (i.e., the system is not confluent). In 1981 Huet showed that even if the system is not confluent, the Knuth-Bendix procedure still yields a semi-decision procedure for word problems, provided that every equation can be oriented. In this paper we show that even if some equations are not orientable, the Knuth-Bendix procedure can still be modified into a reasonably efficient semi-decision procedure for word problems in equational theories. Thus, we have lifted the noetherian requirement in the Knuth-Bendix procedure. Several confluence results, extensions, and experiments are given. So are some comparisons with related work. The proof of completeness, which is an interesting subject by itself, employs a new proof technique which utilizes a notion of transfinite semantic trees designed for proving refutational completeness of theorem proving methods in general. The outline of the paper is as follows: Section 1 briefly introduces term rewriting. The unfailing Knuth-Bendix procedure and confluence results are given in Section 2, together with some discussions and comparisons. Section 3 extends the results to a more general theory which includes inequalities. Simplification strategies are given in Section 4. In Section 5 we present the completeness proofs, as well as a framework of theorem proving strategies which captures the deletion strategies and fairness of search plans. Section 6 describes an implementation with some experimental results. Section contains some comparisons and discussions. Research reported in this paper is supported in part by the NSF grant DCS-8401624 and the Greco de Programmation of France.</div></front></TEI><affiliations><list><country><li>France</li><li>États-Unis</li></country><region><li>Grand Est</li><li>Lorraine (région)</li><li>État de New York</li></region><settlement><li>Vandœuvre-lès-Nancy</li></settlement></list><tree><country name="États-Unis"><region name="État de New York"><name sortKey="Hsiang, Jieh" sort="Hsiang, Jieh" uniqKey="Hsiang J" first="Jieh" last="Hsiang">Jieh Hsiang</name></region></country><country name="France"><region name="Grand Est"><name sortKey="Rusinowitch, Michael" sort="Rusinowitch, Michael" uniqKey="Rusinowitch M" first="Michael" last="Rusinowitch">Michael Rusinowitch</name></region></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 00E606 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 00E606 | 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é= ISTEX:92B2614133F8484DD858A5615D802B1CE3E0BD8D
|texte= On word problems in equational theories
}}
| This area was generated with Dilib version V0.6.33. |  |