Reasoning with open logic programs

Abstract

This paper motivates and introduces entailment problems over nonmonotonic theories some of whose predicates - called open predicates - are not (completely) specified. More precisely, we are interested in those inferences that hold for some or all possible axiomatizations of the open predicates. Since a complete specification of an open predicate may model incomplete knowledge about the world, this kind of inference should distinguish missing object-level knowledge from missing parts of the specification, and restrict nonmonotonic inference accordingly. We formalize some interesting forms of such open entailment problems, and provide formal proof techniques for some of them in a logic programming framework. © Springer-Verlag Berlin Heidelberg 2001.