Partial Orders, Residuation, and First-Order Linear Logic
This work addresses proof-theoretic and linguistic challenges in logic, but it appears incremental as it builds on existing first-order linear logic frameworks.
The paper tackles the problem of proof search efficiency in first-order linear logic by introducing partial order constraints that uniquely order antecedent formulas, which also enables the definition of useful logical operators. The result is an improvement in proof search efficiency, though no concrete numbers are provided.
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.