**James Harland**

to appear in a **Special Issue of Computer Languages**

One of the key features of logic programming is the notion of
*goal-directed* provability. In intuitionistic logic, the
notion of *uniform proof* 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 suitably
weaker than that for intuitionistic logic. We show the completeness
of this class of proofs for certain fragments, which thus form logic
programming languages. As there are more possible variations on the
notion of goal-directed provability in classical logic, there is a
greater diversity of classical logic programming languages than
intuitionistic ones. In particular, we show how logic programs may
contain disjunctions in this setting. This provides a proof-theoretic
basis for disjunctive logic programs, as well as characterising the
``disjunctive'' nature of answer substitutions for such programs in
terms of the provability properties of the classical connectives
and
.

**James Harland**

**Journal of Logic and Computation 4:1:69-88, January, 1994.**

Uniform proofs have been presented as a basis for logic programming, and it is known that by restricting the class of formulae it is possible to guarantee that uniform proofs are complete with respect to provability in intuitionistic logic. In this paper we explore the relationship between uniform proofs and classes of formulae more deeply. Firstly we show that uniform proofs arise naturally as a normal form for proofs in first-order intuitionistic sequent calculus. Next we show that the class of formulae known as hereditary Harrop formulae are intimately related to uniform proofs, and that we may extract such formulae from uniform proofs in two different ways. We also give results which may be interpreted as showing that hereditary Harrop formulae are the largest class of formulae for which uniform proofs are guaranteed to be complete. Finally we briefly discuss some possibilities for a slightly more general approach using intermediate and infinitary logics. Paper

**James Harland**

**Journal of Logic Programming 17:1:1-29, October, 1993.**

We introduce the foundational issues involved in incorporating the Negation as Failure (NAF) rule into the framework of first-order hereditary Harrop formulae of Miller et al. This is a larger class of formulae than Horn clauses, and so the technicalities are more intricate than in the Horn clause case. As programs may grow during execution in this framework, the role of NAF and the Closed World Assumption (CWA) need some modification, and for this reason we introduce the notion of a completely defined predicate, which may be thought of as a localisation of the CWA. We also show how this notion may be used to define a notion of NAF for a more general class of goals than literals alone. We also show how an extensional notion of universal quantification may be incorporated. This makes our framework somewhat different from that of Miller et al., but not essentially so. We also show how to construct a Kripke-like model for the extended class of programs. This is essentially a denotational semantics for logic programs, in that it provides a mapping from the program to a pair of sets of atoms which denote the success and (finite) failure sets. This is inspired by the work of Miller on the semantics of first-order hereditary Harrop formulae. Note that no restriction on the class of programs is needed in this approach, and that our construction needs no more than omega iterations. This necessitates a slight departure from the standard methods, but the important properties of the construction still hold. Paper

**James Harland**

**Proceedings of the Fourteenth Australian Computer Science
Conference, Sydney, February, 1991. Published as Australian Computer
Science Communications:13:1, 1991. **

Miller has shown that disjunctions are not necessary in a large fragment of hereditary Harrop formulae, a class of formulae which properly includes Horn clauses. In this paper we extend this result to include existential quantifications, so that for each program P, there is a program P' which is operationally equivalent, but contains no disjunctions or existential quantifications. We may think of this process as deriving a normal form for the program. This process is carried out by pushing the connectives outwards from the body of a clause, and this process leads to a normal form for goals as well. The properties of the search process used to find uniform proofs of goals (which generalises SLD-resolution) together with the normal form allow successful goals to be converted into program clauses, and so we may add successful goals to the program. The stored form of the goal requires a larger class of formulae, i.e. full first-order hereditary Harrop formulae, and so this leads to a natural separation into an object level and a meta-level. This separation seems intuitively natural and to correspond to aspects of programming methodology. Finally we discuss some possibilities for amalgamation of the object and meta-level languages. Paper

**James Harland**

**Proceedings of the International Conference on Logic Programming
711-725, Paris, June, 1991. **

The Clark completion of a program is a way of making explicit the
inferences which may be made from the program using the Negation as
Failure (NAF) rule. This may be thought of as adding negative
information to the program in such a way that an atom fails iff its
negation is derivable from the completion of the program. We show how
the completion process may be extended to hereditary Harrop formulae,
a class of formulae that properly includes Horn clauses, and, more
importantly, that the completion of a hereditary Harrop formula
program may be expressed as a hereditary Harrop formula program. In
fact, we show there are two ways to perform such a completion: one way
which preserves inference, and another in which inconsistencies are
detected. Moreover, we show that the two notions coincide for
*locally consistent* programs, a class which properly includes
locally stratified programs. In addition, we show how the completion
may be used to generate complementary definitions under some
circumstances, so that predicates such as odd and even may be
synthesised from each other.
Paper

**James Harland**

**
Proceedings of the Fifteenth Australasian Computer Science
Conference 337-349, Hobart, January, 1992. **

One of the distinguishing features of logic programming seems to
be the notion of *goal-directed* provability, i.e. that the
structure of the goal is used to determine the next step in the proof
search process. It is known that by restricting the class of formulae
it is possible to guarantee that a certain class of proofs, known as
*uniform proofs*, are complete with respect to provability in
intuitionistic logic. In this paper we explore the relationship
between uniform proofs and classes of formulae more deeply. Firstly we
show that uniform proofs arise naturally as a normal form for proofs
in first-order intuitionistic sequent calculus. Next we show that the
class of formulae known as hereditary Harrop formulae are intimately
related to uniform proofs, and that we may extract such formulae from
uniform proofs in two different ways. We also give results which may
be interpreted as showing that hereditary Harrop formulaeare the
largest class of formulae for which uniform proofs are guaranteed to
be complete, along the lines of an interpolation theorem.
Paper

**James Harland**

**
Proceedings of the Joint International Conference and Symposium on
Logic Programming 146-160, Washington DC, November, 1992. **

It is known that larger classes of formulae than Horn clauses may
be used as logic programming languages. One such class of formulae is
* hereditary Harrop formulae*, for which an operational notion of
provability has been studied, and it is known that operational
provability corresponds to provability in intuitionistic logic. In
this paper we discuss the notion of a normal form for this class of
formulae, and show how this may be given by removing disjunctions and
existential quantifications from programs. Whilst the normal form of
the program preserves operational provability, there are operationally
equivalent programs which are not intuitionistically equivalent. As it
is known that classical logic is too strong to precisely capture
operational provability for larger classes of programs than Horn
clauses, the appropriate logic in which to study questions of
equivalence is an intermediate logic. We explore the nature of the
required logic, and show that this may be obtained by the addition of
the * Independence of Premise* axioms to intuitionistic logic. We
show how equivalence in this logic captures the notion of operational
provability, in that logically equivalent programs are operationally
equivalent. This result suggests that the natural logic in which to
study logic programming is a slightly stronger constructive logic than
intuitionistic logic.
Paper

**James Harland**

**
Proceedings of the Workshop on Proof-Theoretical Extensions of Logic
Programming 10-18, Santa Marghertia Ligure, June, 1994.**

**James Harland**

**
Proceedings of the Workshop on Proof-Theoretical Extensions of Logic
Programming 19-27, Santa Marghertia Ligure, June, 1994.**