A decision procedure for the system E (of entailment). I (Q802540)

The system E is an axiom system together with rules of inference for sentential logic that formalizes a notion of entailment so that it depends on logical content [\textit{A. R. Anderson}, Z. Math. Logik Grundlagen Math. 6, 201-216 (1960; Zbl 0095.008)]. A recursive procedure is provided for determining for any formula, whether or not it is a theorem of E. The procedure is given for a system \(E_ d\) of natural deduction that is equivalent to E. It makes use of restrictions on the applications of rules of inference so that the number of possible applications of rules in searching for a proof will be finite.