This graduate course provides an introduction to linear logic with an emphasis on its applications in computer science.
is one of the world's major centers of research in artificial intelligence.
of a Linear Logic Theorem Prover (llprover) (1998) – This program finds a cut-free proof of a given sequent (however, cut rules are used when axioms are given). That is, it creates a proof from bottom to up by applying applicable rules.
SML/NJ web pages,
including the Basis web pages
This paper describes a compiler system of a linear logic programming language called LLP. New features of LLP with various example programs are also shown. LLP is a superset of Prolog and a subset of Lolli. LLP programs are compiled into LLPAM (LLP Abstract Machine) code, which is an extended WAM (Warren Abstract Machine) designed for LLP. Keywords: Logic programming, Linear logic, Warren Abstract Machine
)Girard, J.-Y. : Linear Logic, Theoretical Computer Science, London Mathematical 50:1, pp. 1-102, 1987. Restored by Pierre Boudes.
Cours de thÃ©orie de la dÃ©monstration, Roma Tre, Octobre-DÃ©cembre 2004.
The Blind Spot
Lectures on proof-theory, Roma Tre, October-December 2004. English translation.
is an innovative software development company, located in Denton, Texas. We specialize in Java and Prolog based Internet programming and Intelligent Mobile Agent building tools