In this chapter, we study various forms of negation. Since only positive information can be a logical consequence of a program, special rules are needed to deduce negative information. The most important of these rules are the closed world assumption and the negation as failure rule. This chapter introduces normal programs, which are programs for which the body of a program clause is a conjunction of literals. The major results of this chapter are soundness and completeness theorems for the negation as failure rule and SLDNF-resolution for normal programs.
KeywordsLogical Consequence Identity Relation Unification Algorithm Equality Theory Predicate Symbol
Unable to display preview. Download preview PDF.