Combining decision algorithms for matching in the union of disjoint equational theories
Identifieur interne : 000D39 ( PascalFrancis/Corpus ); précédent : 000D38; suivant : 000D40Combining decision algorithms for matching in the union of disjoint equational theories
Auteurs : C. RingeissenSource :
- Information and computation [ 0890-5401 ] ; 1996.
Descripteurs français
- Pascal (Inist)
English descriptors
Abstract
This paper addresses the problem of systematically building a matching algorithm for the union of two disjoint theories Ei u E2 provided that matching algorithms are known in both theories E1 and E2. In general, the blind use of combination techniques introduces unification. Two different restrictions are considered in order to reduce this unification to matching. First, we show that combining matching algorithms ( with linear constant restriction ) is always sufficient for solving a pure fragment of combined matching problems. Second, the investigated method is complete for the largest class of theories where unification is not needed, including regular collapse-free theories and linear theories. Syntactic conditions are given to define this class of theories in which solving the combined matching problem is performed in a modular way.
Notice en format standard (ISO 2709)
Pour connaître la documentation sur le format Inist Standard.
| pA |
|
|---|
Format Inist (serveur)
| NO : | PASCAL 96-0319471 INIST |
|---|---|
| ET : | Combining decision algorithms for matching in the union of disjoint equational theories |
| AU : | RINGEISSEN (C.) |
| AF : | INRIA-Lorraine and CRIN-CNRS, Technopôle de Nancy-Brabois-Campus Scientifique, 615, rue du Jardin Botanique, BP 101/54602 Villers-lès-Nancy/France (1 aut.) |
| DT : | Publication en série; Niveau analytique |
| SO : | Information and computation; ISSN 0890-5401; Coden INFCEC; Etats-Unis; Da. 1996; Vol. 126; No. 2; Pp. 144-160; Bibl. 17 ref. |
| LA : | Anglais |
| EA : | This paper addresses the problem of systematically building a matching algorithm for the union of two disjoint theories Ei u E2 provided that matching algorithms are known in both theories E1 and E2. In general, the blind use of combination techniques introduces unification. Two different restrictions are considered in order to reduce this unification to matching. First, we show that combining matching algorithms ( with linear constant restriction ) is always sufficient for solving a pure fragment of combined matching problems. Second, the investigated method is complete for the largest class of theories where unification is not needed, including regular collapse-free theories and linear theories. Syntactic conditions are given to define this class of theories in which solving the combined matching problem is performed in a modular way. |
| CC : | 001D02A05; 001D02B07B |
| FD : | Algorithme; Problème combinatoire; Arbre décision; Concordance forme; Restriction ordre |
| ED : | Algorithms; Combinatorial problem; Decision tree; Pattern matching; Order restriction |
| SD : | Problema combinatorio; Arbol decisión |
| LO : | INIST-8341.354000044137130040 |
| ID : | 96-0319471 |
Links to Exploration step
Pascal:96-0319471Le document en format XML
<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en" level="a">Combining decision algorithms for matching in the union of disjoint equational theories</title><author><name sortKey="Ringeissen, C" sort="Ringeissen, C" uniqKey="Ringeissen C" first="C." last="Ringeissen">C. Ringeissen</name><affiliation><inist:fA14 i1="01"><s1>INRIA-Lorraine and CRIN-CNRS, Technopôle de Nancy-Brabois-Campus Scientifique, 615, rue du Jardin Botanique, BP 101</s1><s2>54602 Villers-lès-Nancy</s2><s3>FRA</s3><sZ>1 aut.</sZ></inist:fA14></affiliation></author></titleStmt><publicationStmt><idno type="wicri:source">INIST</idno><idno type="inist">96-0319471</idno><date when="1996">1996</date><idno type="stanalyst">PASCAL 96-0319471 INIST</idno><idno type="RBID">Pascal:96-0319471</idno><idno type="wicri:Area/PascalFrancis/Corpus">000D39</idno></publicationStmt><sourceDesc><biblStruct><analytic><title xml:lang="en" level="a">Combining decision algorithms for matching in the union of disjoint equational theories</title><author><name sortKey="Ringeissen, C" sort="Ringeissen, C" uniqKey="Ringeissen C" first="C." last="Ringeissen">C. Ringeissen</name><affiliation><inist:fA14 i1="01"><s1>INRIA-Lorraine and CRIN-CNRS, Technopôle de Nancy-Brabois-Campus Scientifique, 615, rue du Jardin Botanique, BP 101</s1><s2>54602 Villers-lès-Nancy</s2><s3>FRA</s3><sZ>1 aut.</sZ></inist:fA14></affiliation></author></analytic><series><title level="j" type="main">Information and computation</title><title level="j" type="abbreviated">Inf. comput.</title><idno type="ISSN">0890-5401</idno><imprint><date when="1996">1996</date></imprint></series></biblStruct></sourceDesc><seriesStmt><title level="j" type="main">Information and computation</title><title level="j" type="abbreviated">Inf. comput.</title><idno type="ISSN">0890-5401</idno></seriesStmt></fileDesc><profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>Algorithms</term><term>Combinatorial problem</term><term>Decision tree</term><term>Order restriction</term><term>Pattern matching</term></keywords><keywords scheme="Pascal" xml:lang="fr"><term>Algorithme</term><term>Problème combinatoire</term><term>Arbre décision</term><term>Concordance forme</term><term>Restriction ordre</term></keywords></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">This paper addresses the problem of systematically building a matching algorithm for the union of two disjoint theories E<sub>i</sub> u E<sub>2</sub> provided that matching algorithms are known in both theories E<sub>1</sub> and E<sub>2</sub>. In general, the blind use of combination techniques introduces unification. Two different restrictions are considered in order to reduce this unification to matching. First, we show that combining matching algorithms ( with linear constant restriction ) is always sufficient for solving a pure fragment of combined matching problems. Second, the investigated method is complete for the largest class of theories where unification is not needed, including regular collapse-free theories and linear theories. Syntactic conditions are given to define this class of theories in which solving the combined matching problem is performed in a modular way.</div></front></TEI><inist><standard h6="B"><pA><fA01 i1="01" i2="1"><s0>0890-5401</s0></fA01><fA02 i1="01"><s0>INFCEC</s0></fA02><fA03 i2="1"><s0>Inf. comput.</s0></fA03><fA05><s2>126</s2></fA05><fA06><s2>2</s2></fA06><fA08 i1="01" i2="1" l="ENG"><s1>Combining decision algorithms for matching in the union of disjoint equational theories</s1></fA08><fA11 i1="01" i2="1"><s1>RINGEISSEN (C.)</s1></fA11><fA14 i1="01"><s1>INRIA-Lorraine and CRIN-CNRS, Technopôle de Nancy-Brabois-Campus Scientifique, 615, rue du Jardin Botanique, BP 101</s1><s2>54602 Villers-lès-Nancy</s2><s3>FRA</s3><sZ>1 aut.</sZ></fA14><fA20><s1>144-160</s1></fA20><fA21><s1>1996</s1></fA21><fA23 i1="01"><s0>ENG</s0></fA23><fA43 i1="01"><s1>INIST</s1><s2>8341</s2><s5>354000044137130040</s5></fA43><fA44><s0>0000</s0><s1>© 1996 INIST-CNRS. All rights reserved.</s1></fA44><fA45><s0>17 ref.</s0></fA45><fA47 i1="01" i2="1"><s0>96-0319471</s0></fA47><fA60><s1>P</s1></fA60><fA61><s0>A</s0></fA61><fA64 i1="01" i2="1"><s0>Information and computation</s0></fA64><fA66 i1="01"><s0>USA</s0></fA66><fC01 i1="01" l="ENG"><s0>This paper addresses the problem of systematically building a matching algorithm for the union of two disjoint theories E<sub>i</sub> u E<sub>2</sub> provided that matching algorithms are known in both theories E<sub>1</sub> and E<sub>2</sub>. In general, the blind use of combination techniques introduces unification. Two different restrictions are considered in order to reduce this unification to matching. First, we show that combining matching algorithms ( with linear constant restriction ) is always sufficient for solving a pure fragment of combined matching problems. Second, the investigated method is complete for the largest class of theories where unification is not needed, including regular collapse-free theories and linear theories. Syntactic conditions are given to define this class of theories in which solving the combined matching problem is performed in a modular way.</s0></fC01><fC02 i1="01" i2="X"><s0>001D02A05</s0></fC02><fC02 i1="02" i2="X"><s0>001D02B07B</s0></fC02><fC03 i1="01" i2="1" l="FRE"><s0>Algorithme</s0><s3>P</s3><s5>01</s5></fC03><fC03 i1="01" i2="1" l="ENG"><s0>Algorithms</s0><s3>P</s3><s5>01</s5></fC03><fC03 i1="02" i2="X" l="FRE"><s0>Problème combinatoire</s0><s5>37</s5></fC03><fC03 i1="02" i2="X" l="ENG"><s0>Combinatorial problem</s0><s5>37</s5></fC03><fC03 i1="02" i2="X" l="SPA"><s0>Problema combinatorio</s0><s5>37</s5></fC03><fC03 i1="03" i2="X" l="FRE"><s0>Arbre décision</s0><s5>38</s5></fC03><fC03 i1="03" i2="X" l="ENG"><s0>Decision tree</s0><s5>38</s5></fC03><fC03 i1="03" i2="X" l="SPA"><s0>Arbol decisión</s0><s5>38</s5></fC03><fC03 i1="04" i2="X" l="FRE"><s0>Concordance forme</s0><s5>39</s5></fC03><fC03 i1="04" i2="X" l="ENG"><s0>Pattern matching</s0><s5>39</s5></fC03><fC03 i1="05" i2="1" l="FRE"><s0>Restriction ordre</s0><s4>CD</s4><s5>96</s5></fC03><fC03 i1="05" i2="1" l="ENG"><s0>Order restriction</s0><s4>CD</s4><s5>96</s5></fC03><fN21><s1>218</s1></fN21></pA></standard><server><NO>PASCAL 96-0319471 INIST</NO><ET>Combining decision algorithms for matching in the union of disjoint equational theories</ET><AU>RINGEISSEN (C.)</AU><AF>INRIA-Lorraine and CRIN-CNRS, Technopôle de Nancy-Brabois-Campus Scientifique, 615, rue du Jardin Botanique, BP 101/54602 Villers-lès-Nancy/France (1 aut.)</AF><DT>Publication en série; Niveau analytique</DT><SO>Information and computation; ISSN 0890-5401; Coden INFCEC; Etats-Unis; Da. 1996; Vol. 126; No. 2; Pp. 144-160; Bibl. 17 ref.</SO><LA>Anglais</LA><EA>This paper addresses the problem of systematically building a matching algorithm for the union of two disjoint theories E<sub>i</sub> u E<sub>2</sub> provided that matching algorithms are known in both theories E<sub>1</sub> and E<sub>2</sub>. In general, the blind use of combination techniques introduces unification. Two different restrictions are considered in order to reduce this unification to matching. First, we show that combining matching algorithms ( with linear constant restriction ) is always sufficient for solving a pure fragment of combined matching problems. Second, the investigated method is complete for the largest class of theories where unification is not needed, including regular collapse-free theories and linear theories. Syntactic conditions are given to define this class of theories in which solving the combined matching problem is performed in a modular way.</EA><CC>001D02A05; 001D02B07B</CC><FD>Algorithme; Problème combinatoire; Arbre décision; Concordance forme; Restriction ordre</FD><ED>Algorithms; Combinatorial problem; Decision tree; Pattern matching; Order restriction</ED><SD>Problema combinatorio; Arbol decisión</SD><LO>INIST-8341.354000044137130040</LO><ID>96-0319471</ID></server></inist></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/PascalFrancis/Corpus
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 000D39 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/PascalFrancis/Corpus/biblio.hfd -nk 000D39 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= PascalFrancis
|étape= Corpus
|type= RBID
|clé= Pascal:96-0319471
|texte= Combining decision algorithms for matching in the union of disjoint equational theories
}}
| This area was generated with Dilib version V0.6.33. |  |