Gentzen-type or Beth-type Systems, Constructive Completeness Proofs and Practical Decision Procedures (with Special Attention to Relevance Logic)

  • H. C. M. de Swart


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.


Formal Proof Atomic Formula Intuitionistic Logic Systematic Procedure Disjunctive Normal Form 
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. Anderson, A. and Belnap, N., 1975, “Entailment: The Logic of Necessity and Relevance,” Princeton University Press, Princeton.Google Scholar
  2. Beth, E., 1959, “The Foundations of Mathematics,” North-Holland, Amsterdam.Google Scholar
  3. Charlwood, G., 1981, An Axiomatic Version of Positive Semilattice Relevance Logic, The Journal of Symbolic Logic, 46:233–239.CrossRefGoogle Scholar
  4. Fitting, M., 1969, “Intuitionistic Logic, Model Theory and Forcing,” North-Holland, Amsterdam.Google Scholar
  5. Kleene, S. C., 1962, Disjunction and Existence under Implication in Elementary Intuitionistic Formalisms, The Journal of Symbolic Logic, 27:11–17.CrossRefGoogle Scholar
  6. Kripke, S., 1959, The Problem of Entailment, The Journal of Symbolic Logic, 24:324.Google Scholar
  7. Kron, A., 1978, Decision Procedures for two Positive Relevance Logics, Reports on Mathematical Logic, 10:61–78.Google Scholar
  8. Smullyan, R., 1971, “First Order Logic,” Springer Verlag, Berlin.Google Scholar
  9. Swart, H. C. M. de, 1976, Another Intuitionistic Completeness Proof, The Journal of Symbolic Logic, 41:644–662.CrossRefGoogle Scholar
  10. 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
  11. Swart, H. C. M. de, 1983, A Gentzen-type or Beth-type System, a Practical Decision Procedure and a Constructive Completeness Proof for the Counterfactual Logics VC and VCS, The Journal of Symbolic Logic, 48:1–20.CrossRefGoogle Scholar
  12. Urquhart, A., 1971, Completeness of Weak Implication, Theoria, 37:274–282.CrossRefGoogle Scholar
  13. Urquhart, A., 1972, Semantics for Relevant Logics, The Journal of Symbolic Logic, 37:159–169.CrossRefGoogle Scholar
  14. Urquhart, A., 198., The Undecidability of Entailment and Relevant Implication. To appear.Google Scholar

Copyright information

© Springer Science+Business Media New York 1985

Authors and Affiliations

  • H. C. M. de Swart
    • 1
  1. 1.Tilburg UniversityThe Netherlands

Personalised recommendations