Logic programming in a fragment of intuitionistic linear logic

摘要: The intuitionistic notion of context is refined by using a fragment J.-Y. Girard's (Theor. Comput. Sci., vol.50, p.1-102, 1987) linear logic that includes additive and multiplicative conjunction, implication, universal quantification, the course exponential, constants for empty erasing contexts. It shown has goal-directed interpretation. also nondeterminism results from need to split contexts in order prove conjunction can be handled viewing proof search as process takes context, consumes part it, returns rest (to consumed elsewhere). Examples taken theorem proving, natural language parsing, database programming are presented: each example requires linear, rather than intuitionistic, modeled adequately. >