Table of Contents
Fetching ...

Logic Programming with Multiplicative Structures

Matteo Acclavio, Roberto Maieli

TL;DR

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 is demonstrated.

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

Logic Programming with Multiplicative Structures

TL;DR

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 is demonstrated.

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).
Paper Structure (7 sections, 4 equations, 1 figure)

This paper contains 7 sections, 4 equations, 1 figure.

Figures (1)

  • Figure 1: A summary of the interpretation of proofs-as-programs in the paradigms of functional programming, and logic programming using sequent calculus and using proof net expansion.

Theorems & Definitions (3)

  • Definition 2
  • Definition 3: Orthogonality dan:reg:89
  • Example 4