zbMATH — the first resource for mathematics

A uniform proof-theoretic investigation of linear logic programming. (English) Zbl 0797.03054
The 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)

03F03 Proof theory in general (including proof-theoretic semantics)
03B20 Subsystems of classical logic (including intuitionistic logic)
68N17 Logic programming
PDF BibTeX Cite
Full Text: DOI