**James Harland and Michael Winikoff**

**Proceedings of the JICSLP'98 Workshop on Transactions and Change in
Logic Databases (Dynamics'98) 43-58, Manchester, June, 1998. **

Logic programming languages based on linear logic have been of recent interest, particularly as such languages provide a logical basis for programs which execute within a dynamic environment. Most of these languages are implemented using standard resolution or backward-chaining techniques. However, there are applications for which the use of forward-chaining techniques within a dynamic environment are appropriate, such as genetic algorithms, active databases and agent-based systems, and for which it is difficult or impossible to specify an appropriate goal in advance. In this paper we discuss the foundations for a forward-chaining approach (or in logic programming parlance, a bottom-up approach) to the execution of linear logic programs, which thus provides forward-chaining within a dynamic environment. In this way it is possible not only to execute programs in a forward-chaining manner, but also to combine forward- and backward-chaining execution. We describe and discuss the appropriate inference rules for such a system, the formal results about such rules, the role of search strategies, and applications. Paper

**Tatjana Lutovac and James Harland**

**Proceedings of the CADE14 Workshop on Strategies in Automated
Deduction Townsville, July, 1997.**

Logic programs consist of formulas of mathematical logic and various proof-theoretic techniques can be used to design and analyse execution models for such programs. We briefly review the main problems, which are questions that are still elusive in the design of logic programming languages, from a proof-theoretic point of view. Existing strategies which lead to the various languages are all rather sophisticated and involve complex manipulations of proofs. All are designed for analysis on paper by a human and many of them are ripe for automation. We aim to perform the automation of some aspects of strategies for logic programming language, in order to assist in the design of these languages. In this paper we describe the first steps towards the design of such an automatic analysis tool. We investigate the usage of particular proof manipulations for the analysis of logic programming strategies. We propose a more precise specification of sequent calculi inference rules that we use as a framework for the generalisation and automation-oriented specification of the permutation process. Paper

**Tatjana Lutovac and James Harland**

**Technical Report 97-30, Department of Computer Science, RMIT, April,1997.**

Logic programs consist of formulas of mathematical logic and various proof-theoretic techniques can be used to design and analyse execution models for such programs. We briefly review the main problems, which are questions that are still elusive in the design of logic programming languages, from a proof-theoretic point of view. Existing approaches and analyses which lead to the various languages are all rather sophisticated and involve complex manipulations of proofs. All are designed for analysis on paper by a human and many of them are ripe for automation. We aim to perform the automation of some aspects of proof-theoretic analyses, in order to assist in the design of logic programming languages. In this paper we describe the first steps towards the design of such an automatic analysis tool. We propose a more precise specification of sequent calculi inference rules that we use for the generalisation and automation-oriented specification of permutation process. We illustrate different problems and proposed solutions through the examples in various formulations of sequent calculi for classical, intuitionistic, linear, modal, minimal logic, including single-conclusioned and multiple-conclusioned systems. Paper

**James Harland and David Pym**

to appear in the
**Proceedings of the Fourteenth International Conference on Automated
Deduction (CADE-14), Townsville, July, 1997. **

Proof-search (the basis of logic programming) with multiplicative inference rules, such as linear logic's R and L, is problematic because of the required non-deterministic splitting of resources. Similarly, searching with additive rules such as L and R requires a non-deterministic choice between two formulae. Many strategies which resolve such non-determinism, either locally or globally, are available.

We present a characterization of a range of strategies for distributing and selecting resources in linear sequent calculus proof-search via a sequent calculus annotated with Boolean constraints. Strategies are characterized by calculations of solutions of sets of Boolean equations generated by searches. Our characterization encompasses lazy (or local), eager (or global) and intermediate (mixed local and global) strategies. Paper

**James Harland, David Pym and Michael Winikoff**

**Proceedings of the Fifth International Conference on Algebraic
Methodology and Software Technology 391-405, Munich, July,
1996.**

Recently, there has been much interest in the derivation of logic
programming languages based on linear logic, a logic of
resource-consumption. Such languages provide a notion of
resource-oriented programming, often leading to programs that are more
elegant and concise than their equivalents in languages, such as
Prolog, based on classical logics. We discuss, with examples, the design,
implementation and applications of *Lygon*, a linear logic
programming language derived from a proof-theoretic analysis of which
occurrences of the linear connectives provide an adequate basis for
programming. In common with other linear logic programming languages,
Lygon allows clauses to be used exactly once in a computation, thereby
avoiding the need for the explicit resource-counting often necessary
in Prolog-like languages. Just as linear logic is a strict
extension of classical logic, Lygon is a strict extension of (pure)
Prolog: all (pure) Prolog programs can be executed by the Lygon
system. Hence all the features of classical pure logic programs are
available in Lygon, together with new ones based on linear
logic. These include *global variables*, a theoretically
transparent notion of *state*, *mutual exclusion
operators* and various constructs for manipulating clauses. All of
these follow from the basis of Lygon in linear logic and *do not
require* extra-logical features for their definition.
Paper

**Michael Winikoff and James Harland**

**Proceedings of the Nineteenth Australasian Computer Science
Conference 262-271, Melbourne, January, 1996. **

We describe and discuss the applications of a logic programming
language called *Lygon*. This language is based on linear logic, a
logic designed with bounded resources in mind. Linear logic may be
thought of as a generalisation of classical logic, and as a result
Lygon contains various features which do not exist in (pure)
Prolog, whilst maintaining all the features of (pure) Prolog. In this
paper we describe various applications of this language, which include
graph problems, and problems involving states and actions. In logic
programming languages based on classical logic, it is possible to
write elegant solutions for problems over acyclic graphs. By making
use of properties of linear logic, it is possible to write similarly
elegant solutions for cyclic graphs as well. As linear logic enables
changes of state to be neatly expressed, it is straightforward to give
Lygon solutions to problems such as the Yale shooting problem and the
blocks world, and we give example solutions to each.
Paper

**Michael Winikoff and James Harland**

**
Proceedings of the International Logic Programming Symposium 66-80, Portland, Decemeber, 1995.
**

There has been considerable work aimed at enhancing the expressiveness of logic programming languages. To this end logics other than classical first order logic have been considered, including intuitionistic, relevant, temporal, modal and linear logic. Girard's linear logic has formed the basis of a number of logic programming languages. These languages are successful in enhancing the expressiveness of (pure) Prolog and have been shown to provide natural solutions to problems involving concurrency, natural language processing, database processing and various resource oriented problems. One of the richer linear logic programming languages is Lygon. In this paper we investigate the implementation of Lygon. Two significant problems that arise are the division of resources between sub-branches of the proof and the selection of the formula to be decomposed. We present solutions to both of these problems. Paper

**Michael Winikoff and James Harland**

**
Proceedings of the Eighteenth Australasian Computer Science
Conference 563-572, Adelaide, February, 1995. **

We describe and discuss the implementation of a new logic programming
language called *Lygon*. This language is based on linear logic, a
logic designed with bounded resources in mind. Linear logic may be thought
of as a generalisation of classical logic, and as a result *Lygon*
contains various features which do not exist in (pure) Prolog, whilst
maintaining all the features of (pure) Prolog. In this paper we describe
the implementation of this language, which posed a variety of programming
challenges. The operational model for the language is based on the notion
of *goal-directed* provability, a notion which has been much studied in
the literature. However, there is a significant amount of non-determinism
in this notion of proof. Hence the task of developing a systematic and
deterministic manner in which to search for proofs requires some intricate
and novel implementation techniques. We describe and discuss our
particular solution, as well as the features of the language and its
applications.
Paper

**David Pym and James Harland**

**Journal of Logic and Computation 4:2:175-207, April, 1994.**

In this paper we consider the problem of identifying logic programming languages for linear logic. Our analysis builds on a notion of goal-directed provability, characterized by the so-called uniform proofs, previously introduced for minimal and intuitionistic logic. A class of uniform proofs in linear logic is identified by an analysis of the permutability of inferences in the linear sequent calculus. We show that this class of proofs is complete (for logical consequence) for a certain (quite large) fragment of linear logic, which thus forms a logic programming language. We obtain a notion of resolution proof, in which only one left rule, of clause-directed resolution, is required. We also consider a translation, resembling those of Girard, of the hereditary Harrop fragment of intuitionistic logic into our framework. We show that goal-directed provability is preserved under this translation. Paper

**James Harland and David Pym**

**Proceedings of the Seventeenth Annual Computer Science
Conference 647-658, Christchurch, January, 1994. **

Traditional logic programming languages, such as Prolog, have their origins
in classical logic. Recently it has been shown how logic programming
languages can be based on linear logic, a logic designed with bounded
resources in mind. In this paper we discuss the implementation issues for
the linear logic programming language *Lygon*, and describe some of the
novel features of the language. These include global variables, a notion of
state, mutual exclusion operators and constructs for the manipulation of
clauses. We also show how a bin packing problem can be solved simply and
elegantly in Lygon.
Paper

**James Harland and David Pym**

**Proceedings of the Russian Conference on Logic Programming and
Automated Reasoning 30-41, St. Petersburg, July, 1992. Published as
Lecture Notes in Artificial Intelligence 624, Springer-Verlag, 1992.**

We present a proof-theoretic foundation for logic programming in Girard's linear logic. We exploit the permutability properties of two-sided linear sequent calculus to identify appropriate notions of uniform proof, definite formula, goal formula, clause and resolution proof for fragments of linear logic. The analysis of this paper extends earlier work by the present authors to include negative occurrences of par and positive occurrences of ! (of course !) and ? (why not ?). These connectives introduce considerable difficulty. We consider briefly some of the issues related to the mechanical implementation of our resolution proofs. Paper

**James Harland and David Pym**

**Proceedings of the International Logic Programming Symposium 304-318, San Diego, October, 1991.**

We present a proof-theoretic analysis of a natural notion of * logic
programming* for Girard's *linear logic*. This analysis enables us to
identify a suitable notion of *uniform proof*. This in turn enables us
to identify choices of classes of definite and goal formulae for which
uniform proofs are complete and so to obtain the appropriate formulation of
*resolution proof* for such choices. Resolution proofs in linear
logic are somewhat difficult to define. This difficulty arises from the
need to decompose definite formulae into a form suitable for the use of the
linear resolution rule, a rule which requires the selected clause to be
*deleted* after use, and from the presence of the *modality* !
(of course).
We consider a *translation* --- resembling those of Girard ---
of the intuitionistic hereditary Harrop formulae
and intuitionistic uniform proofs into our framework, and show that
certain properties are preserved under this translation.
We sketch the design of an *interpreter* for linear logic programs.
Paper