A Modular Approach to Proving Confluence
We are interested in investigating the confluence properties of cooperating constraint solvers. To this end, we model solvers as reductions that transform constraint networks, we define the notion of insensitivity to a superset relation, and show that, if each solver of a given set of solvers is insensitive to the same terminating superset relation, then any combination of these solvers is confluent. By means of this modular approach, we study the relationship between confluence and maintaining certain levels of local consistency and we demonstrate the confluence of a solver for a global finite-domain constraint that consists of several reductions.
Unable to display preview. Download preview PDF.
- 2.F. Baader and T. Nipkow. Term Rewriting and All That. Cambridge University Press, 1998.Google Scholar
- 4.M. Marte. A global constraint for parallelizing the execution of task sets. Technical Report PMS-FB-2001-13, Institut für Informatik der Universität München, 2001.Google Scholar
- 5.M. Marte. A modular approach to proving confluence. Technical Report PMS-FB-2001-18, Institut für Informatik der Universität München, 2001.Google Scholar