Disunification is the problem of deciding satisfiability of a system of equations and disequations w.r.t. a given equational theory. In this paper we study the disunification problem in the context of ACI1 equational theories. We provide a characterization of the interpretation structures suitable to model the axioms in ACI1 theories. The satisfiability problem is solved using known techniques for the equality constraints and novel methodologies to transform disequation constraints into solved forms. We propose three solved forms, offering an increasingly more precise characterization of the set of solutions. Two of them can be computed and tested in polynomial time. The novel results achieved open new possibilities in the practical and efficient manipulation of ACI1 constraints.

ACI1 Constraints

DOVIER, Agostino;PIAZZA, Carla;
1999

Abstract

Disunification is the problem of deciding satisfiability of a system of equations and disequations w.r.t. a given equational theory. In this paper we study the disunification problem in the context of ACI1 equational theories. We provide a characterization of the interpretation structures suitable to model the axioms in ACI1 theories. The satisfiability problem is solved using known techniques for the equality constraints and novel methodologies to transform disequation constraints into solved forms. We propose three solved forms, offering an increasingly more precise characterization of the set of solutions. Two of them can be computed and tested in polynomial time. The novel results achieved open new possibilities in the practical and efficient manipulation of ACI1 constraints.
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: http://hdl.handle.net/11390/739860
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? 0
social impact