Logic programming in a fragment of intuitionistic linear logic
Logic programming in a fragment of intuitionistic linear logic
复制标题
直觉线性逻辑片段中的逻辑编程
DOI：
--
复制
发表时间：
1991
期刊：
影响因子：
--
通讯作者：
D. Miller
中科院分区：
文献类型：
--
作者：
J. S. Hodas;D. Miller
上下文的直觉主义概念通过使用j - y的片段得到了改进。吉拉德(定理。第一版。科学。线性逻辑，包括加性和乘性合取、线性蕴涵、普适量化、当然指数、空上下文和擦除上下文的常数。结果表明，该逻辑具有目标导向的解释。本文还表明，为了证明乘法连接而需要分割上下文所导致的不确定性，可以通过将证明搜索视为一个过程来处理，该过程接受上下文，使用其中的一部分，并返回其余部分（将在其他地方使用）。本文给出了取自定理证明、自然语言解析和数据库编程的例子：每个例子都需要一个线性的、而不是直观的上下文概念来充分建模
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.<<ETX>>