Relevant logic programming (Q1181715)

Several authors suggested extension of Horn clause programming using bottom-up proof search in Gentzen-type systems for intuitionistic logic with suitable restriction of the language. The author describes a similar program based on the relevance logic LR\(^ +\) without negation and distributivity axiom. Language is restricted to banish negative occurrences of disjunction. For this fragment, relevance logic R is conservative over RL\(^ +\) as the author conjectured. This is Corollary 1 in the reviewer's paper [Zap. Nauchn. Semin. Leningr. Otd. Mat. Inst. Steklova 32, 90-97 (1973; Zbl 0374.02017)] .