In the logic programming paradigm, a program is defined by a set of methods, each of which can be executed when specific conditions are met during the current state of an execution. The semantics of these programs can be elegantly represented using sequent calculi, in which each method is linked to an inference rule. In this context, proof search mirrors the program's execution. Previous works introduced a framework in which the process of constructing proof nets is employed to model executions, as opposed to the traditional approach of proof search in sequent calculus. This paper further extends this investigation by focussing on the pure multiplicative fragment of this framework. We demonstrate, providing practical examples, the capability to define logic programming methods with context-sensitive behaviors solely through specific resource-preserving and context-free operations, corresponding to certain generalized multiplicative connectives explored in existing literature. We show how some of these methods, although still multiplicative, escape the purely multiplicative fragment of Linear Logic (MLL).
翻译:在逻辑编程范式中,程序由一组方法定义,每个方法可在执行当前状态下满足特定条件时被执行。这些程序的语义可优雅地使用相继式演算表示,其中每个方法对应一个推理规则。在此框架下,证明搜索反映了程序的执行过程。先前研究提出了一个采用证明网构造过程来建模执行的框架,以区别于传统的相继式演算证明搜索方法。本文通过聚焦于该框架的纯乘法片段进一步拓展此项研究。我们通过实例证明,仅需借助特定的资源保持与上下文无关操作(对应于现有文献中探讨的某些广义乘法连接词),即可定义具有上下文敏感行为的逻辑编程方法。我们展示了其中部分方法虽仍属乘法范畴,却超越了线性逻辑的纯乘法片段(MLL)。