Mutually Exclusive Modules in Logic Programming

TL;DR

This paper introduces choice-conjunctive modules in logic programming, enabling explicit representation of mutually exclusive modules using linear logic connectives, thereby addressing a longstanding limitation.

Contribution

It proposes a novel module construct using linear logic to express mutual exclusivity in logic programming, with formal operational semantics.

Findings

Defines choice-conjunctive modules with linear logic

Provides operational semantics for mutually exclusive modules

Enables explicit mutual exclusion in logic programming

Abstract

Logic programming has traditionally lacked devices for expressing mutually exclusive modules. We address this limitation by adopting choice-conjunctive modules of the form $D_0 \& D_1$ where $D_0, D_1$ are a conjunction of Horn clauses and $\&$ is a linear logic connective. Solving a goal $G$ using $D_0 \& D_1$ -- $exec(D_0 \& D_1,G)$ -- has the following operational semantics: $choose$ a successful one between $exec(D_0,G)$ and $exec(D_1,G)$. In other words, if $D_0$ is chosen in the course of solving $G$, then $D_1$ will be discarded and vice versa. Hence, the class of choice-conjunctive modules can capture the notion of mutually exclusive modules.