Choice Disjunctive Queries in Logic Programming

TL;DR

This paper proposes a high-level logical approach to handle the cut predicate in logic programming by using linear logic and choice-disjunctive goals, enabling mutually exclusive task specification.

Contribution

It introduces a novel method using linear logic and choice-disjunctive goals to treat the cut predicate in a logical, high-level manner.

Findings

Allows high-level specification of mutually exclusive tasks

Provides a logical semantics for the cut predicate

Enables execution of one goal while discarding others

Abstract

One of the long-standing research problems on logic programming is to treat the cut predicate in a logical, high-level way. We argue that this problem can be solved by adopting linear logic and choice-disjunctive goal formulas of the form $G_0 \add G_1$ where $G_0, G_1$ are goals. These goals have the following intended semantics: $choose$ the true disjunct $G_i$ and execute $G_i$ where $i (= 0\ {\rm or}\ 1)$, while $discarding$ the unchosen disjunct. Note that only one goal can remain alive during execution. These goals thus allow us to specify mutually exclusive tasks in a high-level way.