TITLE: ``Soundness and Completeness versus Lifting Property''

ABSTRACT:

We will give new formulations of the property of soundness and completeness of a resolution system and of the lifting lemma, and discuss their relationship. The discussion will point 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 will be demonstrated on the case of basic variants of the SLDNF-resolution. If time allows, we will mention results of a joint research project with Dr. Stephen Murrell which is devoted to the development of the theory of a complete resolution system and to implementation of LOGOS - a truly declarative (untyped) logic programming language.

Everyone is welcome to attend.