Combination of Constraint Solvers

Welcome to the reserch project Combination of Constraint Solvers at the CIS, University of Munich, Germany.
This is a cooperative project, our partners are located in Aachen.

This project is funded by the DFG (German Research Council) as part of the national focus programme on automated deduction. We also receive travel subsistence by the European Union.

Project Description

Staff

Publications

Implementation

Description of the Combination Project

Specialised methods for solving special deduction problems deliver an important contribution for extending and accelerating universal deduction components. Consequently, one is confronted with the problem of coupling the specialised method with the universal one and with coupling different special methods. In the case of special unification procedures modulo disjunctive equational theories, these combination problems have been subject of intensive research.

The aim of this research project is twofold. Firstly, we want to implement the existing combination methods as efficient as possible and thereby provide them as tools to other members of the research community. To do so, we plan to develop concepts of optimisations for specific classes of equational theories, especially for the combination of decision procedures for unification.
On a more abstract level, we intend to generalise existing combination methods, for example for cases of non-disjoint theories and problems more general that term unification. Our final aim is to gain a better understanding of the fundamental algorithmic problems in combination of specific deduction procedures and to develop a rather generally applicable combination algorithm.

Final Report to the DFG. (Available only in German.)

Staff of Combination Project

Professor

Prof. Dr. Klaus U. Schulz

Assistant

Dr. Stephan Kepser

Stephan Kepser