Constructive Negation in Logic Programs
Abstract
This work lays solid groundwork for systematic study of negation in logic programming that preserves the declarative nature of the languages like pure PROLOG, can be efficiently executed without major changes to present interpreters, and allows programs to retain their constructive solutions. Transformation of positive predicates into their negative duals can introduce universal quantification in the body of the defining clause. Constructive implementation of universal quantifiers in general requires unbounded searches, but in an important subcase implementation is practical. Frequently, the universally quantified formula is an implication, allowing the antecedent to filter instantiations of the consequent. The SLD resolution procedure was modified to handle this situation, and explored circumstances under which the resulting executions are practical. Logic programming is declarative, but its programs can be executed relatively efficiently. This balance is a precarious one: languages with a more imperative nature are much faster in execution, but programming is more difficult; if the declarative expressiveness of the language is extended, its execution can become so slow that it is unusable. The languages typified by 'pure' PROLOG strike this balance on the side of efficiency, by fixing on SLD resolution as the execution algorithm. The Horn-clause subset of first-order logic for which SLD resolution is adequate is limited in the naturalness of its expressiveness, and the most notable omission is that negative information cannot be expressed.
Document Details
- Document Type
- Technical Report
- Publication Date
- Jan 01, 1987
- Accession Number
- ADA196562
Entities
People
- Richard Hamlet