
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 \textit{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.
Proof theory in general (including proof-theoretic semantics), linear logic, goal-to-subgoal proof search, Subsystems of classical logic (including intuitionistic logic), Logic programming
Proof theory in general (including proof-theoretic semantics), linear logic, goal-to-subgoal proof search, Subsystems of classical logic (including intuitionistic logic), Logic programming
| selected citations These citations are derived from selected sources. This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | 40 | |
| popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network. | Average | |
| influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | Top 10% | |
| impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network. | Top 10% |
