ON GOAL-DIRECTED PROVABILITY IN CLASSICAL-LOGIC

One of the key features of logic programming is the notion of goal-dir ected provability. In intuitionistic logic, the notion of uniform proo f has been used as a proof-theoretic characterization of this property . Whilst the connections between intuitionistic logic and computation are well known, there is no reason per se why a similar notion cannot be given in classical logic. In this paper we show that there are two notions of goal-directed proof in classical logic, both of which are s uitably weaker than that for intuitionistic logic. We show the complet eness of this class of proofs for certain fragments, which thus form l ogic programming languages. As there are more possible variations on t he notion of goal-directed provability in classical logic, there is a greater diversity of classical logic programming languages than intuit ionistic ones. In particular, we show how logic programs may contain d isjunctions in this setting. This provides a proof-theoretic basis for disjunctive logic programs, as well as characterising the ''disjuncti ve'' nature of answer substitutions for such programs in terms of the provability properties of the classical connectives There Exists and b oolean AND. (C) 1997 Elsevier Science Ltd. All rights reserved.