Logic Programming with Multiplicative Structures

TL;DR

This paper extends the framework of logic programming semantics using sequent calculi and proof nets, focusing on multiplicative structures to model context-sensitive, resource-preserving methods beyond traditional linear logic.

Contribution

It introduces a way to define context-sensitive logic programming methods within the multiplicative fragment, expanding the applicability of proof net models.

Findings

Demonstrates resource-preserving, context-free operations for logic programming methods.

Shows some methods extend beyond the purely multiplicative fragment of Linear Logic.

Provides practical examples of multiplicative logic programming techniques.

Abstract

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).