{C}ombination of {U}nification {A}lgorithms for {N}on-Disjoint {E}quational {T}heories
Identifieur interne : 003295 ( Crin/Checkpoint ); précédent : 003294; suivant : 003296{C}ombination of {U}nification {A}lgorithms for {N}on-Disjoint {E}quational {T}heories
Auteurs : E. Domenjoud ; F. Klay ; Ch. RingeissenSource :
Abstract
We consider here the combination of non-disjoint theories, and give sufficient conditions under which algorithms for solving the word problem, the matching problem and the unification problem in the union may be built automatically from algorithms for each theory. The problem is obviously unsolvable in general, and we restrict our attention to theories sharing constructors which have to be defined in a suitable way. This restriction is however still not sufficient in general. Indeed, some properties like simplicity, which turns out to be very useful for unification, are lost when combining theories sharing constructors. A theory is simple if a term is never equivalent to one of its strict subterms. If we consider the theories presented respectively by fgx=hx and khx=gx, which share the constructors h and g according to our definition, we have kfgx=gx modulo their union which is thus not simple. Each of these theories is however obviously simple.
Links toward previous steps (curation, corpus...)
Links to Exploration step
CRIN:domenjoud93bLe document en format XML
<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en" wicri:score="768">{C}ombination of {U}nification {A}lgorithms for {N}on-Disjoint {E}quational {T}heories</title></titleStmt><publicationStmt><idno type="RBID">CRIN:domenjoud93b</idno><date when="1993" year="1993">1993</date><idno type="wicri:Area/Crin/Corpus">001267</idno><idno type="wicri:Area/Crin/Curation">001267</idno><idno type="wicri:explorRef" wicri:stream="Crin" wicri:step="Curation">001267</idno><idno type="wicri:Area/Crin/Checkpoint">003295</idno><idno type="wicri:explorRef" wicri:stream="Crin" wicri:step="Checkpoint">003295</idno></publicationStmt><sourceDesc><biblStruct><analytic><title xml:lang="en">{C}ombination of {U}nification {A}lgorithms for {N}on-Disjoint {E}quational {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><author><name sortKey="Ringeissen, Ch" sort="Ringeissen, Ch" uniqKey="Ringeissen C" first="Ch." last="Ringeissen">Ch. Ringeissen</name></author></analytic></biblStruct></sourceDesc></fileDesc><profileDesc><textClass></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en" wicri:score="3151">We consider here the combination of non-disjoint theories, and give sufficient conditions under which algorithms for solving the word problem, the matching problem and the unification problem in the union may be built automatically from algorithms for each theory. The problem is obviously unsolvable in general, and we restrict our attention to theories sharing constructors which have to be defined in a suitable way. This restriction is however still not sufficient in general. Indeed, some properties like simplicity, which turns out to be very useful for unification, are lost when combining theories sharing constructors. A theory is simple if a term is never equivalent to one of its strict subterms. If we consider the theories presented respectively by fgx=hx and khx=gx, which share the constructors h and g according to our definition, we have kfgx=gx modulo their union which is thus not simple. Each of these theories is however obviously simple.</div></front></TEI><BibTex type="inproceedings"><ref>domenjoud93b</ref><crinnumber>93-R-305</crinnumber><category>5</category><equipe>PROTHEO</equipe><author><e>Domenjoud, E.</e><e>Klay, F.</e><e>Ringeissen, Ch.</e></author><title>{C}ombination of {U}nification {A}lgorithms for {N}on-Disjoint {E}quational {T}heories</title><booktitle>{Presented at UNIF'93, Boston (USA)}</booktitle><year>1993</year><month>jun</month><abstract>We consider here the combination of non-disjoint theories, and give sufficient conditions under which algorithms for solving the word problem, the matching problem and the unification problem in the union may be built automatically from algorithms for each theory. The problem is obviously unsolvable in general, and we restrict our attention to theories sharing constructors which have to be defined in a suitable way. This restriction is however still not sufficient in general. Indeed, some properties like simplicity, which turns out to be very useful for unification, are lost when combining theories sharing constructors. A theory is simple if a term is never equivalent to one of its strict subterms. If we consider the theories presented respectively by fgx=hx and khx=gx, which share the constructors h and g according to our definition, we have kfgx=gx modulo their union which is thus not simple. Each of these theories is however obviously simple.</abstract></BibTex></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Crin/Checkpoint
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 003295 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Crin/Checkpoint/biblio.hfd -nk 003295 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Crin
|étape= Checkpoint
|type= RBID
|clé= CRIN:domenjoud93b
|texte= {C}ombination of {U}nification {A}lgorithms for {N}on-Disjoint {E}quational {T}heories
}}
| This area was generated with Dilib version V0.6.33. |  |