Sixth Annual IEEE Symposium on

Logic in Computer Science (LICS 1991)

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

Authors: Joshua S. Hodas Dale Miller


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


    author = 	 {Joshua S. Hodas and Dale Miller},
    title = 	 {Logic programming in a fragment of intuitionistic linear logic},
    booktitle =  {Proceedings of the Sixth Annual IEEE Symp. on Logic in Computer Science, {LICS} 1991},
    year =	 1991,
    editor =	 {Giles Kahn},
    month =	 {July}, 
    pages =      {32--42},
    location =   {Amsterdam, The Netherlands}, 
    publisher =	 {IEEE Computer Society Press}