Implementation and Development Issues for the Linear Logic Programming Language Lygon

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 signi cant amount of nondeterminism 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