ACID-Unification is NEXPTIME-Decidable

Siva Anantharaman; Paliath Narendran; Michaël Rusinowitch

hal-00080663, version 1

ACID-Unification is NEXPTIME-Decidable

Siva Anantharaman (), Paliath Narendran () ^1, 2, Michaël Rusinowitch () ^1, 3

(2003) 169--178

Abstract: We consider the unification problem for the equational theory AC(U)ID obtained by adjoining a binary `*' which is distributive over an associative-commutative idempotent operator `+', possibly admitting a unit element U. We formulate the problem as a particular class of set constraints, and propose a method for solving it by using the dag automata introduced by W. Charatonik, that we enrich with labels for our purposes. AC(U)ID-unification is thus shown to be in NEXPTIME.

1: Laboratoire d'Informatique Fondamentale d'Orléans (LIFO)
Université d'Orléans : EA4022 – Ecole Nationale Supérieure d'Ingénieurs de Bourges
2: Department of Computer Science [Albany] (CS)
State University of New York at Albany
3: CASSIS (INRIA Lorraine - LORIA / LIFC)
INRIA – CNRS : FRE2661 – Université de Franche-Comté – Université Henri Poincaré - Nancy I – Université Nancy II – Institut National Polytechnique de Lorraine (INPL)

hal-00080663, version 1
http://hal.archives-ouvertes.fr/hal-00080663
oai:hal.archives-ouvertes.fr:hal-00080663
From: Siva Anantharaman <>
Submitted on: Tuesday, 20 June 2006 08:44:38
Updated on: Wednesday, 17 January 2007 15:40:03

See detailed view

Export

Bibtex EndNote TEI RefWorks

<?xml version="1.0" encoding="UTF-8"?>
<listBibl xmlns="http://www.tei-c.org/ns/1.0" xmlns:xlink="http://www.w3.org/1999/xlink" xmlns:mml="http://www.w3.org/1998/Math/MathML">
<listBibl type="inproceedings"><head>Peer-reviewed conferences/proceedings</head>
<biblStruct type="inproceedings" xml:id="hal-00080663"><analytic>
<author><persName><forename>Siva</forename><surname>Anantharaman</surname></persName></author>
<author><persName><forename>Paliath</forename><surname>Narendran</surname></persName>
<affiliation>
<orgName type="laboratory">LIFO</orgName>
<orgName type="team">Laboratoire d'Informatique Fondamentale d'Orléans</orgName>
<country>FR</country>
<orgName type="institution">Université d'Orléans : EA4022</orgName>
<orgName type="institution">Ecole Nationale Supérieure d'Ingénieurs de Bourges</orgName>
</affiliation>
<affiliation>
<orgName type="laboratory">CS</orgName>
<orgName type="team">Department of Computer Science [Albany]</orgName>
<country>US</country>
<orgName type="institution">State University of New York at Albany</orgName>
</affiliation>
</author>
<author><persName><forename>Michaël</forename><surname>Rusinowitch</surname></persName>
<affiliation>
<orgName type="laboratory">LIFO</orgName>
<orgName type="team">Laboratoire d'Informatique Fondamentale d'Orléans</orgName>
<country>FR</country>
<orgName type="institution">Université d'Orléans : EA4022</orgName>
<orgName type="institution">Ecole Nationale Supérieure d'Ingénieurs de Bourges</orgName>
</affiliation>
<affiliation>
<orgName type="laboratory">INRIA Lorraine - LORIA / LIFC</orgName>
<orgName type="team">CASSIS</orgName>
<country>FR</country>
<orgName type="institution">INRIA</orgName>
<orgName type="institution">CNRS : FRE2661</orgName>
<orgName type="institution">Université de Franche-Comté</orgName>
<orgName type="institution">Université Henri Poincaré - Nancy I</orgName>
<orgName type="institution">Université Nancy II</orgName>
<orgName type="institution">Institut National Polytechnique de Lorraine (INPL)</orgName>
</affiliation>
</author>
<title type="main" level="a">ACID-Unification is NEXPTIME-Decidable</title></analytic><monogr><title level="m" type="main">Mathematical Foundations of Computer Science 2003</title><imprint><publisher>Springer-Verlag</publisher><biblScope type="publicationDate">2003-00-00</biblScope><biblScope type="pp">169--178</biblScope></imprint></monogr><idno type="HALid">http://hal.archives-ouvertes.fr/hal-00080663</idno></biblStruct>
</listBibl>
</listBibl>