Problem solving by equivalent transformation of negative constraints

This paper proposes a new approach to negation. While most theories for negation are based on the logic paradigm, our theory is constructed based on the equivalent transformation (ET) computation model, since the ET computation model provides us with "decomposability of programs." A negative constraint has a domain that is the complement of the semantics of the corresponding declarative description. Computation of negation in the ET paradigm is realized by equivalent transformation of declarative descriptions including negative constraints. For each negative constraint in a definite clause, a new declarative description is produced and transformed equivalently. When it is transformed to a set of unit clauses, the negative constraint is solved. Each unit clause returns a simple constraint to the "caller" clause. This paper proves two theorems that provide a basis for such equivalent transformation of negative constraints.