We consider propositional programs in a logic programming language which allows implications in the bodies of rules. Given a program P in such a language and a goal g the relation "P implies g" may be conceived as derivability in intuitionistic logic of the formula g from the set P of premisses. In general, however, logic programming languages do not admit the full syntax of intuitionistic logic for writing program rules. N-Prolog, for instance, has rules of the form B —> h, where h is an atom or the constant 1 and B is a conjunction of an arbitrary number of atoms and rules. Goals are atoms or the constant _L (cf. [1]), In order to determine, whether a program P implies a goal g ("P ? g succeeds") a so called goal directed calculus is used, which in essence is a version of denizen's calculus NJ of natural deduction. It is built on the observation that in an NJ-deduction of an atom a from a set of N-Prolog rules the final inference has to be an application of modus ponens. Therefore P must contain a rule of the form B -> a and B must be derivable from P. But B is a conjunction, therefore each of its conjuncts has to be derivable from P and in turn each of the conjuncts is either an atom or an implication C —> i. In the latter case we know that /' must be derivable from P,C. But this set is again a program, so we are back in the situation we had started with, having obtained a new program and a new goal to derive from it.
展开▼
