Soundness and completeness versus lifting property
We give new formulations of the property of soundness and completeness of a resolution system and of the lifting lemma, and we discuss their relationship.
The discussion points out why certain resolution systems are not complete, and that there is a simple method for showing that a resolution system is “absolutely incomplete” — that there is no notion of program completion and no logic which could give soundness and completeness. The method is demonstrated on the case of basic variants of the SLDNF-resolution. The same approach can be used to analyze other resolution systems.
Keywordssoundness and completeness lifting lemma program completion SLDNF-resolution
Unable to display preview. Download preview PDF.
- [Chan88]D. Chan, Constructive Negation Based on Completed Database, in [LPconf88], pp. 111–125.Google Scholar
- [Chan89]D. Chan, An extension of constructive negation and its application in corouting, in [LPconfNA89], pp. 477–493.Google Scholar
- [Clark78]K. L. Clark, Negation as Failure, in Logic and Databases, edited by H. Gallaire and J. Minker, Plenum Press, New York, 1978, pp. 193–322.Google Scholar
- [Clark79]K. L. Clark, Predicate Logic as a Computational Formalism, Research Report DOC 79/59, Dept. of Computing, Imperial College, 1979.Google Scholar
- [Doets94]K. Doets, From Logic to Logic Programming MIT Press, 1994.Google Scholar
- [DM91]W. Drabent and M.Martelli, Strict Completion of Logic Programs, New Generation Computing 9, pp. 69–79, 1991.Google Scholar
- [Drabent95]What is Failure? An Approach to Constructive Negation, Acta Informatica, to appear.Google Scholar
- [Kunen87]K. Kunen, Answer Sets and Negation as Failure, in [LPconf87].Google Scholar
- [Lloyd87]J. W. Lloyd, Foundations of Logic Programming, Second extended edition, Springer Verlag, 1987.Google Scholar
- [LPconf87]J-L. Lassez (ed.), Logic Programming, Proceedings of the Fourth International Conference, MIT Press, 1987.Google Scholar
- [LPconf88]R. A. Kowalski and K. A. Bowen (eds.), Logic Programming, Proceedings of the Fifth International Conference and Symposium, MIT Press, 1988.Google Scholar
- [LPconfNA89]E. L. Lusk and R. A. Overbeek (eds.), Logic Programming, Proceedings of the North American Conference 1989, MIT Press, 1989.Google Scholar
- [O'Keefe90]R. A. O'Keefe, The Craft of Prolog, MIT Press, 1990.Google Scholar
- [Plaza90]J. A. Plaza, Fully Declarative Programming with Logic — Mathematical Foundations Ph.D. Dissertation, City University of New York, July 1990.Google Scholar
- [Plaza91]J. A. Plaza, Completeness for propositional logic programs with negation, in: Methodologies for Intelligent Systems, 6th International Symposium, edited by Z. W. Ras and M. Zemankova, Springer Verlag, LNAI 542, 1991, pp. 600–609.Google Scholar
- [Plaza92f]J. A. Plaza, Fully Declarative Logic Programming, in Programming Language Implementation and Logic Programming, 4th International Symposium, edited by M. Bruynooghe and M. Wirsing, Springer Verlag, LNCS 631, 1992, pp. 415–427.Google Scholar
- [Plaza92o]J. A. Plaza, Operators on Lattices of omega-Herbrand Interpretations, in: A. Nerode and M. Taitslin (eds.) Logical Foundations of Computer Science — Tver '92, Second International Symposium, Tver, Russia, July 1992, Proceedings, Springer Verlag, LNCS 620, 1992 pp. 358–369.Google Scholar
- [Przymusiński89]T. C. Przymusiński, On Constructive Negation in Logic Programming, in [LPconfNA89], addendum.Google Scholar