Conditional Narrowing with Constructive Negation

Author

María José Ramírez, Moreno Falaschi

Abstract

In this paper, we present a narrower for conditional equational theories whose clauses allow disequations in their bodies (normal theories). Our approach deals with disequations in a constructive manner and thus allows non ground negative queries. We give a formal operational semantics for normal theories and define the notion of completion and stratification of a normal theory. We show that there exists one minimal model for the completion of a stratified normal theory. Then we prove the correctness of the operational semantics with respect to the completion of a stratified normal theory.

Keywords

Equational logic programming, constructive negation, term rewriting systems, narrowing.