Gentzen-type or Beth-type Systems, Constructive Completeness Proofs and Practical Decision Procedures (with Special Attention to Relevance Logic)
The aim of this paper is to advertise a notion of provability, originally known as Beth-semantic tableaux (Beth, 1959), then later adapted by R. Smullyan (1971) for classical logic and by M. Fitting (1969) for intuitionistic logic and for the modal system S4.
KeywordsFormal Proof Atomic Formula Intuitionistic Logic Systematic Procedure Disjunctive Normal Form
Unable to display preview. Download preview PDF.
- Anderson, A. and Belnap, N., 1975, “Entailment: The Logic of Necessity and Relevance,” Princeton University Press, Princeton.Google Scholar
- Beth, E., 1959, “The Foundations of Mathematics,” North-Holland, Amsterdam.Google Scholar
- Fitting, M., 1969, “Intuitionistic Logic, Model Theory and Forcing,” North-Holland, Amsterdam.Google Scholar
- Kripke, S., 1959, The Problem of Entailment, The Journal of Symbolic Logic, 24:324.Google Scholar
- Kron, A., 1978, Decision Procedures for two Positive Relevance Logics, Reports on Mathematical Logic, 10:61–78.Google Scholar
- Smullyan, R., 1971, “First Order Logic,” Springer Verlag, Berlin.Google Scholar
- Swart, H. C. M. de, 1980, Gentzen-type Systems for C., K and Several Extensions of C and K, Logique et Analyse, 90/91:263–284.Google Scholar
- Urquhart, A., 198., The Undecidability of Entailment and Relevant Implication. To appear.Google Scholar