Negation as failure as resolution

Chandru, Vijay ; Roy, Suman ; Subrahmanyam, Ramesh (1998) Negation as failure as resolution Constraints, 3 (4). pp. 315-329. ISSN 1383-7133

Full text not available from this repository.

Official URL:

Related URL:


Providing a clean procedural semantics of the Negation As Failure rule in Logic Programming has been an open problem for some time now. This rule has been treated as a technique in nonmonotonic reasoning, not as a rule in classical logic. This paper contains a demonstration of the negation as failure rule as a resolution procedure in first-order logic. We present a sound and complete resolution scheme for negation as failure rule for the larger class of constraint logic programs. The approach is to consider a canonical partition of the completion of a definite (constraint) program into the IF and the FI programs. We show that a negated goal, provable from the completed definite program is provable from just the FI part. The clauses in this program have a structure dual to that of definite Horn clauses. We describe a sound and complete linear resolution rule for this fragment, and show that a resolution proof of the negated goal from the FI part corresponds to a finite failure tree resulting from classical linear resolution applied to the goal on the If part of the original definite program. Our work shows that negation as failure rule can be computationally efficient in the sense that the SLD-resolution on the If part of a definite program along with the negation as failure rule is more efficient than a direct resolution procedure on the completion of that program.

Item Type:Article
Source:Copyright of this article belongs to Springer-Verlag.
Keywords:Constraint Logic Programming; Nonmonotonic Reasoning; Negation as Failure; SLD-derivation
ID Code:5525
Deposited On:19 Oct 2010 12:01
Last Modified:22 Oct 2010 06:24

Repository Staff Only: item control page