A CORRECT RULE-BASED GEOMETRIC CONSTRAINT SOLVER

We present a rule-based geometric constraint solver. The solver handle s 2-D, variational, constraint-defined geometric objects. The solver c omputes a solution in two phases. First, the solver builds a sequence of construction steps. Then the construction steps are carried out to generate an instance of the geometric object for the current dimension values. We prove that the solver is correct. First, we formalize the solver as a rewrite system whose rewriting rules are geometric constru ction steps. Then we prove that, for well-constrained geometric object s, the sequence in which the solver applies the construction steps def ines a terminating confluent reduction system. (C) 1997 Elsevier Scien ce Ltd. All rights reserved.