Conditional Narrowing with Constructive Negation
María José Ramírez, Moreno Falaschi
In this paper, we present a narrower for conditional equational
theories whose clauses allow disequations in their bodies (normal
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.
Equational logic programming, constructive negation, term rewriting systems,