Shallow {AC} {T}heories
Identifieur interne : 001256 ( Crin/Curation ); précédent : 001255; suivant : 001257Shallow {AC} {T}heories
Auteurs : E. Domenjoud ; F. KlaySource :
English descriptors
- KwdEn :
Abstract
We consider the class of theories presented by a shallow presentation where some function symbols are associative and commutative (AC) with the restriction that no variable occurs below an AC symbol. A presentation is shallow if variables occur at depth at most one in axioms. We show that such a presentation may be completed into a finite canonical rewriting system modulo AC \cup P where P is a finite set of permuters. This gives a uniform method for solving efficiently the word problem in this class. We also show that unifiability is decidable and discuss possible extensions to the case where variable occur below AC symbols.
Links toward previous steps (curation, corpus...)
- to stream Crin, to step Corpus: Pour aller vers cette notice dans l'étape Curation :001256
Links to Exploration step
CRIN:domenjoud93aLe document en format XML
<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en" wicri:score="48">Shallow {AC} {T}heories</title></titleStmt><publicationStmt><idno type="RBID">CRIN:domenjoud93a</idno><date when="1993" year="1993">1993</date><idno type="wicri:Area/Crin/Corpus">001256</idno><idno type="wicri:Area/Crin/Curation">001256</idno><idno type="wicri:explorRef" wicri:stream="Crin" wicri:step="Curation">001256</idno></publicationStmt><sourceDesc><biblStruct><analytic><title xml:lang="en">Shallow {AC} {T}heories</title><author><name sortKey="Domenjoud, E" sort="Domenjoud, E" uniqKey="Domenjoud E" first="E." last="Domenjoud">E. Domenjoud</name></author><author><name sortKey="Klay, F" sort="Klay, F" uniqKey="Klay F" first="F." last="Klay">F. Klay</name></author></analytic></biblStruct></sourceDesc></fileDesc><profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>AC theories</term><term>combination</term><term>completion</term><term>narrowing</term></keywords></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en" wicri:score="1608">We consider the class of theories presented by a shallow presentation where some function symbols are associative and commutative (AC) with the restriction that no variable occurs below an AC symbol. A presentation is shallow if variables occur at depth at most one in axioms. We show that such a presentation may be completed into a finite canonical rewriting system modulo AC \cup P where P is a finite set of permuters. This gives a uniform method for solving efficiently the word problem in this class. We also show that unifiability is decidable and discuss possible extensions to the case where variable occur below AC symbols.</div></front></TEI><BibTex type="techreport"><ref>domenjoud93a</ref><crinnumber>93-R-289</crinnumber><category>15</category><equipe>AUTRE</equipe><author><e>Domenjoud, E.</e><e>Klay, F.</e></author><title>Shallow {AC} {T}heories</title><institution>CRIN</institution><year>1993</year><address>Vandoeuvre-lès-Nancy</address><note>Presented at the second CCL Workshop (La Escala, Spain)</note><keywords><e>combination</e><e>AC theories</e><e>completion</e><e>narrowing</e></keywords><abstract>We consider the class of theories presented by a shallow presentation where some function symbols are associative and commutative (AC) with the restriction that no variable occurs below an AC symbol. A presentation is shallow if variables occur at depth at most one in axioms. We show that such a presentation may be completed into a finite canonical rewriting system modulo AC \cup P where P is a finite set of permuters. This gives a uniform method for solving efficiently the word problem in this class. We also show that unifiability is decidable and discuss possible extensions to the case where variable occur below AC symbols.</abstract></BibTex></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Crin/Curation
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 001256 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Crin/Curation/biblio.hfd -nk 001256 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Crin
|étape= Curation
|type= RBID
|clé= CRIN:domenjoud93a
|texte= Shallow {AC} {T}heories
}}
| This area was generated with Dilib version V0.6.33. |  |