Algorithms for Relevant Logic

  • Paul Gochet
  • Pascal Gribomont
  • Didier Rossetto
Part of the Logic, Epistemology, and the Unity of Science book series (LEUS, volume 2)


The classical analytic tableau method has been extended successfully to modal logics (see e.g. Fitting 1983; Fitting 1993; Goré 1992) and also to relevant and paraconsistent logics Bloesch 1993a; Bloesch 1993b. The classical connection method has been extended to modal and intuitionistic logics Wallen 1990, and the purpose of this paper is to investigate whether a similar adaptation to relevant logic is possible. A hybrid method is developed for B+, with a specific solution to the “multiplicity problem”, as in the technique of modal semantic diagrams introduced in Hughes and Cresswell 1968. Proofs of soundness and completeness are also given.


Atomic Formula Reduction Rule Path Tree Relevant Logic Syntactic Tree 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. Batens D. (2001). “A Dynamic Characterization of the Pure Logic of Relevant Implication”. Journal of philosophical logic 30:267–280.Google Scholar
  2. Bloesch A. (1993). Signed Tableaux — A Basis for Automated Theorem Proving in non Classical Logics. PhD thesis, University of QueenslandGoogle Scholar
  3. ____ (1993). “A Tableau Style Proof System for Two Paraconsistent Logics”, Notre Dame Journal of Formal Logic 34:2, pp.295–301.Google Scholar
  4. Fitting M. (1983). Proof Methods for Modal and Intuitionistic Logics. Dordrecht Reidel Publishing Company.Google Scholar
  5. ____ (1993). “Basic Modal Logic”, Handbook of Logic in Artificial Intelligence and Logic Programming), Ed. by D. M. Gabbay, C. J. Hogger and J. A. Robinson. Oxford Clarendon Press.Google Scholar
  6. Goré R. (1992). Cut-free Sequent and Tableau Systems for Propositional Normal Logic. Technical report, Cambridge.Google Scholar
  7. Gribomont E.P. & Rossetto D. (1995). CAVEAT: Technique and Tool for Computer Aided VErification And Transformation, Lecture Notes in Computer Science 939, Computer Aided Verification. Springer.Google Scholar
  8. Hughes G.E. & Cresswell M.J. (1968). An Introduction to Modal Logic. London Methuen and Co Ltd 1968, 1972.Google Scholar
  9. Priest G. & Sylvan R. (1992). “Simplified Semantics for Basic Relevant Logics”, Journal of Philosophical Logic 21:217–232.Google Scholar
  10. Restall G. (1993). “Simplified Semantics for Relevant Logics (and some of their rivals)”, Journal of Philosophical Logic 22:481–511.Google Scholar
  11. Wallen L. (1990). Automated Proof Search in Non-classical Logics. Cambridge MIT Press.Google Scholar

Copyright information

© Springer 2005

Authors and Affiliations

  • Paul Gochet
    • Pascal Gribomont
      • Didier Rossetto
        • 1
      1. 1.Université de LiègeLiège

      Personalised recommendations