## Paper: Logic programming in a fragment of intuitionistic linear logic (at LICS 1991)

*Winner of the Test-of-Time Award in 2011***Joshua S. Hodas Dale A. Miller**

### Abstract

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

### BibTeX

@InProceedings{HodasMiller-Logicprogrammingina, author = {Joshua S. Hodas and Dale A. Miller}, title = {Logic programming in a fragment of intuitionistic linear logic}, booktitle = {Proceedings of the Sixth Annual IEEE Symposium on Logic in Computer Science (LICS 1991)}, year = {1991}, month = {July}, pages = {32--42}, location = {Amsterdam, The Netherlands}, publisher = {IEEE Computer Society Press} }