A Bottom-up Semantics for Constructive Negation
Pascal Van Hentenryck · 1994
The constructive negation rule has heen introduced by Chan [5, 6] to overcome the main drawbacks of the negation-as-failure rule: the unsoundness of floundering prer grams and, consequently, the inability of providing answers for non-ground negative queries. In this paper we define a bottom-up semantics for constructive negation which we prove sound and complete with respect to the three-valued completion of the program. The semantics describes answers as well as undefined computations for both positive and negative queries. Its construction closely follows the basic idea of constructive negation whereby answers to a negative query are obtained by negating a frontier of the computation tree for the corresponding positive query. Therefore, the proposed semantics can be considered as a natural base for reasoning on the operational semantics for constructive negation defined in the literature. Moreover, we show how the semantics can be effectively used to perform a bottom-up computation of the answers of a normal query.