Tableau formulations are given for the relevance logics E (Entailment), R (Relevant implication) and RM (Mingle). Proofs of equivalence to modus-ponens-based formulations are vialeft-handed Gentzen sequenzen-kalküle. The tableau formulations depend on a detailed analysis of the structure of tableau rules, leading to certain global requirements. Relevance is caught by the requirement that each node must be used; modality is caught by the requirement that only certain rules can cross a barrier. Open problems are discussed.

In [6] proof tableau formulations were given of the implication/negation fragments of the important zero-order relevant logics E and R and the semirelevant logic RM . The main purpose of this paper then, is to extend results by giving proof tableau formulations of the distribution-free fragments of E, R and RM and of their first order extensions EQ, RQ and RMQ. Where X is one of these logics, we shall follow [13] in calling its distribution-free fragment OX – the ‘O’ (...) standing for ‘ortho’ which is meant to signify the kinship of these logics to quantum logics or ortho-logics as they now tend to be known. Hence in what follows we shall refer to the logics OX simply as relevant ortho-logics. (shrink)

This book constitutes the refereed proceedings of the 13th International Conference on Automated Deduction, CADE-13, held in July/August 1996 in New Brunswick, NJ, USA, as part of FLoC '96. The volume presents 46 revised regular papers selected from a total of 114 submissions in this category; also included are 15 selected system descriptions and abstracts of two invited talks. The CADE conferences are the major forum for the presentation of new results in all aspects of automated deduction. Therefore, the volume (...) is a timely report on the state-of-the-art in the area. (shrink)