The relevant logics E, R and N R are given Hilbert-style axiomatizations and are studied in detail in [1]. By dropping the axioms governing the extensional connectives ^ and v from the axiomatizations of these logics we obtain their implication/negation fragments - respectively the system E , R and NR. By adding axioms for the intensional connectives fusion and ssion + to NR, we obtain the pure intensional fragments of the systems R and NR { called in [4] Ri and NRi respectively. By dropping from R just the axiom that governs the distributional properties of ^ and v, i.e. A ^ (B v C) -> (A ^ B) v C, we obtain the system called O R in [10] and studied in this book. A theorem was announced in [3] which was extended in [2], [5] and [7] to show that the relevant logics E, Ri, NRi and O R and the modal S4 are decidable. This theorem was shown in [8] to be equivalent to the numbertheoretic theorem was shown in [8] to be equivalent to the number-theoretic theorem known as Dickson’s theorem (for details of which see [9]). Given any formula A (in the appropriate vocabulary) the decision procedure for each of these logics describes a way of recursively constructing out of A a proof-search which will contain as a sub-tree a proof of A if there is one and which, it is proved will always be nite. However in practice this decision procedure tends to be impossible to use due to the exponential rate at which the proof search tree for A usually grows. Hence in [4] the question of whether this decision procedure could be mechanized via computer was asked.