A uniform proof-theoretic investigation of linear logic programming.

*(English)*Zbl 0797.03054The goal here is to extend to linear logic a proof-search strategy (uniform proofs) for goal-to-subgoal proof search in the Gentzen-type formulation of intuitionistic logic, introduced by D. Miller [J. Logic Program. 6, No. 1/2, 79-108 (1989; Zbl 0681.68022)]. It requires to analyze first the succedent (right-hand side) formula till the atomic goal \(g\) is reached, and then to analyze an antecedent (left-hand side) implication with a conclusion matching \(g\). Using the classical device of permuting inference rules, the authors were able to prove completeness of the strategy they defined for a fragment of linear logic including Girard translations of hereditary Harrop formulas. Usefulness for logic programming can be judged only after the strategy is implemented. Relevant work includes that by the reviewer (which did not include implementation) and that by T. Tammet which describes one of the best existing general-purpose provers for linear logic.

Reviewer: G.Mints (Stanford)