Combination of Constraint Solving Techniques: An Algebraic Point of View

Franz BaaderFranz Baader, Klaus U. SchulzKlaus U. Schulz

Datei:CIS-94-75.ps.gz

Download

Franz Baader, Klaus U. Schulz
Combination of Constraint Solving Techniques: An Algebraic Point of View
Technical Report, Center for Language and Information Processing (CIS), volume CIS-Rep-94-75, July 1994. Research Report

Details
Bibtex

KurzfassungAbstract
In a previous paper we have introduced a method that allows one to combine decision procedures for unifiability in disjoint equational theories. Lately, it has turned out that the prerequisite for this method to apply---namely that unification with so-called linear constant restrictions is decidable in the single theories---is equivalent to requiring decidability of the positive fragment of the first order theory of the equational theories. Thus, the combination method can also be seen as a tool for combining decision procedures for positive theories of free algebras defined by equational theories. The present paper uses this observation as the starting point of a more abstract, algebraic approach to formulating and solving the combination problem. Its contributions are twofold. As a new result, we describe an (optimized) extension of our combination method to the case of constraint solvers that also take relational constraints (such as ordering constraints) into account. The second contribution is a new proof method, which depends on abstract notions and results from universal algebra, as opposed to technical manipulations of terms (such as ordered rewriting, abstraction functions, etc.)
Forschungsgruppe:Research Group: AutomatentheorieAutomata Theory

@techreport{ BaaderSchulz-CIS-94-75,
  address = {Wagm\"ullerstra{\ss}e 23, D-80538 Munich, Germany},
  author = {Franz {Baader} and Klaus U. {Schulz}},
  institution = {Center for Language and Information Processing (CIS)},
  month = {July},
  number = {CIS-Rep-94-75},
  title = {Combination of Constraint Solving Techniques: {A}n Algebraic Point of View},
  type = {Research Report},
  year = {1994},
}