Logic Programming in a Fragment of Intuitionistic Linear Logic: Extended Abstract
Joshua S. Hodas, Dale Armin Miller · 1991
Joshua S. Hodas Dale Miller Computer Science Dept. LFCS, Computer Science Dept. University of Pennsylvania University of Edinburgh, KB Philadelphia, PA 19104-6389 USA Edinburgh EH9 3JZ Scotland [email protected] [email protected] Abstract Logic programming languages based on fragments of intuitionistic logic have recently been developed and studied by several researchers. In such languages, implications are permitted in goals and in the bodies of clauses. Attempting to prove a goal of the form D oe G in a context \\Gamma leads to an attempt to prove the goal G in the extended context \\Gamma [ fDg. While an intuitionistic notion of context has many uses, it has turned out to be either too powerful or too limiting in several settings. We refine the intuitionistic notion of context by using a fragment of Girard's linear logic that includes additive and multiplicative conjunction, linear implication, universal quantification, the "of course" exponential, and the constants 1 (th...