Combination of Constraint Solvers for Free and Quasi-Free Structures

Franz BaaderFranz Baader, K. SchulzK. Schulz

Franz Baader, K. Schulz
Combination of Constraint Solvers for Free and Quasi-Free Structures
Theoretical Computer Science, 192:107-161, 1998

Details
Bibtex

KurzfassungAbstract
When combining languages for symbolic constraints, one is typically faced with the problem of how to treat ``mixed constraints. The two main problems are (1) how to define a combined solution structure over which these constraints are to be solved, and (2) how to combine the constraint solving methods for pure constraints into one for mixed constraints. The paper introduces the notion of a ``free amalgamated product as a possible solution to the first problem. We define so-called quasi-free structures (called ``strong simply-combinable structures in a previous publication) as a generalization of free structures. For quasi-free structures over disjoint signatures, we describe a canonical amalgamation construction that yields the free amalgamated product. The combination techniques known from unification theory can be used to combine constraint solvers for quasi-free structures over disjoint signatures into a solver for their free amalgamated product. In addition to term algebras modulo equational theories (i.e., free algebras), the class of quasi-free structures contains many solution structures that are of interest in constraint logic programming, such as the algebra of rational trees, feature structures, and domains consisting of hereditarily finite (wellfounded or non-wellfounded) nested sets and lists.
Forschungsgruppe:Research Group: AutomatentheorieAutomata Theory

@article{ BaaderSchulz-TCS-98,
  author = {F. {Baader} and K. {Schulz}},
  journal = {Theoretical Computer Science},
  pages = {107--161},
  title = {Combination of Constraint Solvers for Free and Quasi-Free Structures},
  volume = {192},
  year = {1998},
}