Algorithms for Relevant Logic
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.
KeywordsAtomic Formula Reduction Rule Path Tree Relevant Logic Syntactic Tree
Unable to display preview. Download preview PDF.
- Batens D. (2001). “A Dynamic Characterization of the Pure Logic of Relevant Implication”. Journal of philosophical logic 30:267–280.Google Scholar
- Bloesch A. (1993). Signed Tableaux — A Basis for Automated Theorem Proving in non Classical Logics. PhD thesis, University of QueenslandGoogle Scholar
- ____ (1993). “A Tableau Style Proof System for Two Paraconsistent Logics”, Notre Dame Journal of Formal Logic 34:2, pp.295–301.Google Scholar
- Fitting M. (1983). Proof Methods for Modal and Intuitionistic Logics. Dordrecht Reidel Publishing Company.Google Scholar
- ____ (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
- Goré R. (1992). Cut-free Sequent and Tableau Systems for Propositional Normal Logic. Technical report, Cambridge.Google Scholar
- 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
- Hughes G.E. & Cresswell M.J. (1968). An Introduction to Modal Logic. London Methuen and Co Ltd 1968, 1972.Google Scholar
- Priest G. & Sylvan R. (1992). “Simplified Semantics for Basic Relevant Logics”, Journal of Philosophical Logic 21:217–232.Google Scholar
- Restall G. (1993). “Simplified Semantics for Relevant Logics (and some of their rivals)”, Journal of Philosophical Logic 22:481–511.Google Scholar
- Wallen L. (1990). Automated Proof Search in Non-classical Logics. Cambridge MIT Press.Google Scholar