A theoretical foundation of problem solving by equivalent transformation of negative constraints

Representation and computation of negation is very important in problem solving in various application domains. The purpose of this paper is to propose a new approach to negation. While most theories for negation are based on the logic paradigm, this theory is constructed based on the equivalent transformation (ET) computation model, since the ET model provides us with decomposability of programs, i.e., a program in the ET model is a set of ET rules and can be synthesized by generating each ET rule independently of other ET rules. To represent negation in the ET model, a constraint is introduced as a pair of an object and a domain. A constraint becomes true when the object is specialized to a ground object within the domain. A negative constraint has a domain that is the complement of the meaning 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.