{{stub}}{{language|Lygon |site=http://www.cs.rmit.edu.au/lygon/}} Lygon is a logic programming language that is based on linear logic. It can be viewed as [[Prolog]] extended with features derived from linear logic. These features include a declarative notion of state and the ability to express problems involving concurrency. Also, the availability of use once predicates allows simple solutions to problems such as graph manipulation. Although the design of Lygon relies on a delicate proof-theoretic analysis of linear logic, programmers need have no knowledge of proof theory.

Linear logic can be used to model the consumption of resources. Whereas clauses in Prolog, based on classical logic, can be used many times during the execution of a program, clauses in Lygon, based on linear logic, must (by default) be used exactly once. Since both classical and intuitionistic logic can be embedded in linear logic, Lygon generalizes pure Prolog. Indeed, pure Prolog code (Edinburgh syntax) can be executed by Lygon's interpreter.