Towards an efficient tableau proof procedure for multiple-valued logics

  • Reiner Hähnle
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 533)


One of the obstacles against the use of tableau-based theorem provers for non-standard logics is the inefficiency of tableau systems in practical applications, though they are highly intuitive and extremely flexible from a proof theoretical point of view. We present a method for increasing the efficiency of tableau systems in the case of multiple-valued logics by introducing a generalized notion of signed formulas and give sound and complete tableau systems for arbitrary propositional finite-valued logics.


Truth Table Propositional Variable Rule Application Abstract Algebra Proof 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. [Bet86]
    E. W. Beth. Semantic entailment and formal derivability. In Karel Berka and Lothar Kreiser, editors, Logik-Texte. Kommentierte Auswahl zur Geschichte der modernen Logik, pages 262–266. Akademie-Verlag, Berlin, 1986.Google Scholar
  2. [BS81]
    Stanley Burris and H.P. Sankappanavar. A Course in Universal Algebra, volume 78 of Graduate Texts in Mathematics. Springer, New York, 1981.Google Scholar
  3. [Car87]
    Walter A. Carnielli. Systematization of finite many-valued logics through the method of tableaux. Journal of Symbolic Logic, 52(2):473–493, June 1987.Google Scholar
  4. [Due88]
    Gerhard W. Dueck. Algorithms for the Minimization of Binary and Multiple-Valued Logic Functions. PhD thesis, University of Manitoba, Winnipeg, 1988.Google Scholar
  5. [FHLvB85]
    Jens Erik Fenstad, Per-Kristian Halvorsen, Tore Langholm, and Johan von Benthem. Equations, schemata and situations: A framework for linguistic semantics. Technical Report CSLI-85-29, Center for the Studies of Language and Information Stanford, 1985.Google Scholar
  6. [Fit83]
    Melvin C. Fitting. Proof Methods for Modal and Intutionistic Logics. Reidel, Dordrecht, 1983.Google Scholar
  7. [Fit89]
    Melvin C. Fitting. Negation as refutation. In LICS 1989 Proceedings, 1989.Google Scholar
  8. [Fit90]
    Melvin C. Fitting. First-Order Logic and Automated Theorem Proving. Springer, New York, 1990.Google Scholar
  9. [Hä90]
    Reiner Hähnle. Spezifikation eines Theorembeweisers für dreiwertige First-Order Logik. IWBS Report 136, Wissenschaftliches Zentrum, IWBS, IBM Deutschland, September 1990.Google Scholar
  10. [Hä91]
    Reiner Hähnle. Uniform notation of tableaux rules for multiple-valued logics. In To appear in Proceedings International Symposium on Multiple-Valued Logic, Victoria, 1991.Google Scholar
  11. [KW90]
    T. Kropf and H.-J. Wunderlich. Hierarchische Testmustergenerierung für sequentielle Schaltungen mit Hilfe von Temporaler Logik. II. ITG/GI Workshop Testmethoden und Zuverlässigkeit von Schaltungen und Systemen, 1990.Google Scholar
  12. [OS86]
    F. Oppacher and E. Suen. Controlling deduction with proof condensation and heuristics. In Jörg H. Siekmann, editor, Proc. 8th International Conference on Automated Deduction, pages 384–393, 1986.Google Scholar
  13. [OS88]
    F. Oppacher and E. Suen. HARP: A tableau-based theorem prover. Journal of Automated Reasoning, 4:69–100, 1988.CrossRefGoogle Scholar
  14. [Sch89]
    Peter H. Schmitt. Perspectives in multi-valued logic. Proceedings International Scientific Symposium on Natural Language and Logic, Hamburg, 1989.Google Scholar
  15. [She89]
    John C. Sheperdson. A sound and complete semantics for a version of negation as failure. Theoretical Computer Science, 65:343–371, 1989.CrossRefGoogle Scholar
  16. [Smu68]
    Raymond Smullyan. First-Order Logic. Springer, New York, second edition, 1968.Google Scholar
  17. [Sta90]
    Z. Stachniak. Note on resolution approximation of many-valued logics. In 20th International Symposium on Multiple-Valued Logic, Charlotte, pages 204–209, May 1990.Google Scholar
  18. [Sur84]
    Stanisław J. Surma. An algorithm for axiomatizing every finite logic. In David C. Rine, editor, Computer Science and Multiple-Valued Logics, pages 143–149. North-Holland, Amsterdam, 1984.Google Scholar
  19. [Wój88]
    Ryszard Wójcicki. Theory of Logical Calculi. Reidel, Dordrecht, 1988.Google Scholar
  20. [Wol81]
    Pierre Wolper. Temporal logic can be more expressive. In Proceedings 22nd Annual Symposium on Foundations of Computer Science, pages 340–348, 1981.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1991

Authors and Affiliations

  • Reiner Hähnle
    • 1
  1. 1.Institute for Logic, Complexity and Deduction SystemsUniversity of KarlsruheKarlsruheFederal Republic of Germany

Personalised recommendations