Partial Orders, Residuation, and First-Order Linear Logic

TL;DR

This paper explores how partial order constraints in first-order linear logic can define useful logical operators and enhance proof search efficiency, with implications for proof theory and linguistics.

Contribution

It introduces a novel approach of incorporating partial order constraints into first-order linear logic to define new operators and improve proof search.

Findings

Partial order constraints enable defining new logical operators.

Partial orders improve proof search efficiency.

Unique linear orders on antecedents are achievable.

Abstract

We will investigate proof-theoretic and linguistic aspects of first-order linear logic. We will show that adding partial order constraints in such a way that each sequent defines a unique linear order on the antecedent formulas of a sequent allows us to define many useful logical operators. In addition, the partial order constraints improve the efficiency of proof search.