Unification Modulo ACUI Plus Distributivity Axioms
Identifieur interne : 003E89 ( Crin/Corpus ); précédent : 003E88; suivant : 003E90Unification Modulo ACUI Plus Distributivity Axioms
Auteurs : Siva Anantharaman ; Paliath Narendran ; Michael RusinowitchSource :
- Journal of Automated Reasoning ; 2004.
English descriptors
- KwdEn :
Abstract
E-unification problems are central in automated deduction. In this work, we consider unification modulo theories that extend the well-known ACI or ACUI by adding a binary symbol `*' that distributes over the AC(U)I-symbol `+'. If this distributivity is one-sided (say, to the left), we get the theory denoted AC(U)IDl ; we show that AC(U)IDl-unification is DEXPTIME-complete. If `*' is assumed 2-sided distributive over `+', we get the theory denoted AC(U)ID ; we show unification modulo AC(U)ID to be NEXPTIME-decidable and DEXPTIME-hard. Both AC(U)IDl and AC(U)ID seem to be of practical interest, e.g. in the analysis of programs modeled in terms of process algebras. Our results, for the two theories considered, are obtained via two entirely different lines of reasoning. It is a consequence of our methods of proof, that modulo the theory which adds on to AC(U)ID the assumption that `*' is associative-commutative -- or just associative --, unification is undecidable.
Links to Exploration step
CRIN:anantharaman04aLe document en format XML
<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en" wicri:score="295">Unification Modulo ACUI Plus Distributivity Axioms</title>
</titleStmt>
<publicationStmt><idno type="RBID">CRIN:anantharaman04a</idno>
<date when="2004" year="2004">2004</date>
<idno type="wicri:Area/Crin/Corpus">003E89</idno>
</publicationStmt>
<sourceDesc><biblStruct><analytic><title xml:lang="en">Unification Modulo ACUI Plus Distributivity Axioms</title>
<author><name sortKey="Anantharaman, Siva" sort="Anantharaman, Siva" uniqKey="Anantharaman S" first="Siva" last="Anantharaman">Siva Anantharaman</name>
</author>
<author><name sortKey="Narendran, Paliath" sort="Narendran, Paliath" uniqKey="Narendran P" first="Paliath" last="Narendran">Paliath Narendran</name>
</author>
<author><name sortKey="Rusinowitch, Michael" sort="Rusinowitch, Michael" uniqKey="Rusinowitch M" first="Michael" last="Rusinowitch">Michael Rusinowitch</name>
</author>
</analytic>
<series><title level="j">Journal of Automated Reasoning</title>
<imprint><date when="2004" type="published">2004</date>
</imprint>
</series>
</biblStruct>
</sourceDesc>
</fileDesc>
<profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>automated deduction</term>
<term>unification</term>
</keywords>
</textClass>
</profileDesc>
</teiHeader>
<front><div type="abstract" xml:lang="en" wicri:score="2381">E-unification problems are central in automated deduction. In this work, we consider unification modulo theories that extend the well-known ACI or ACUI by adding a binary symbol `*' that distributes over the AC(U)I-symbol `+'. If this distributivity is one-sided (say, to the left), we get the theory denoted AC(U)IDl ; we show that AC(U)IDl-unification is DEXPTIME-complete. If `*' is assumed 2-sided distributive over `+', we get the theory denoted AC(U)ID ; we show unification modulo AC(U)ID to be NEXPTIME-decidable and DEXPTIME-hard. Both AC(U)IDl and AC(U)ID seem to be of practical interest, e.g. in the analysis of programs modeled in terms of process algebras. Our results, for the two theories considered, are obtained via two entirely different lines of reasoning. It is a consequence of our methods of proof, that modulo the theory which adds on to AC(U)ID the assumption that `*' is associative-commutative -- or just associative --, unification is undecidable.</div>
</front>
</TEI>
<BibTex type="article"><ref>anantharaman04a</ref>
<crinnumber>A04-R-189</crinnumber>
<category>1</category>
<equipe>LIFO</equipe>
<author><e>Anantharaman, Siva</e>
<e>Narendran , Paliath</e>
<e>Rusinowitch, Michael</e>
</author>
<title>Unification Modulo ACUI Plus Distributivity Axioms</title>
<journal>Journal of Automated Reasoning</journal>
<year>2004</year>
<volume>33</volume>
<number>1</number>
<pages>1-28</pages>
<month>Dec</month>
<keywords><e>unification</e>
<e>automated deduction</e>
</keywords>
<abstract>E-unification problems are central in automated deduction. In this work, we consider unification modulo theories that extend the well-known ACI or ACUI by adding a binary symbol `*' that distributes over the AC(U)I-symbol `+'. If this distributivity is one-sided (say, to the left), we get the theory denoted AC(U)IDl ; we show that AC(U)IDl-unification is DEXPTIME-complete. If `*' is assumed 2-sided distributive over `+', we get the theory denoted AC(U)ID ; we show unification modulo AC(U)ID to be NEXPTIME-decidable and DEXPTIME-hard. Both AC(U)IDl and AC(U)ID seem to be of practical interest, e.g. in the analysis of programs modeled in terms of process algebras. Our results, for the two theories considered, are obtained via two entirely different lines of reasoning. It is a consequence of our methods of proof, that modulo the theory which adds on to AC(U)ID the assumption that `*' is associative-commutative -- or just associative --, unification is undecidable.</abstract>
</BibTex>
</record>
Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Crin/Corpus
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 003E89 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Crin/Corpus/biblio.hfd -nk 003E89 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien |wiki= Wicri/Lorraine |area= InforLorV4 |flux= Crin |étape= Corpus |type= RBID |clé= CRIN:anantharaman04a |texte= Unification Modulo ACUI Plus Distributivity Axioms }}
![]() | This area was generated with Dilib version V0.6.33. | ![]() |