Skip to main content
SpringerLink
Log in

Propositional logics on the computer

  • Applications
  • Conference paper
  • First Online:
Theorem Proving with Analytic Tableaux and Related Methods (TABLEAUX 1995)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 918))

Abstract

The purpose of the paper is to present the Logics Workbench, an interactive system aiming to facilitate the access to logical formalisms for nonspecialists as well as specialists. It is an integrated system which provides a library of the most important propositional calculi and many algorithms in this area. Special emphasis is put on a clear design of the human interface and a powerful information system, which covers online help and documentation.

Work supported by the Swiss National Science Foundation, SPP 5003-34279.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Jean-Marc Andreoli. Logic programming with focusing proofs in linear logic. Journal of Logic and Computation, 2(3):297–347, 1992.

    Google Scholar 

  2. George Boolos. Provability, truth, and modal logic. Journal of Philosophical Logic, 9:1–7, 1980.

    Article  Google Scholar 

  3. Roy Dyckhoff. Contraction-free sequent calculi for intuitionistic logic. The Journal of Symbolic Logic, 57(3):795–807, 1992.

    Google Scholar 

  4. Melvin Fitting. Proof Methods for Modal and Intuitionistic Logics. Reidel, Dordrecht, 1983.

    Google Scholar 

  5. Melvin Fitting. First-order modal tableaux. Journal of Automated Reasoning, 4:191–213, 1988.

    Article  Google Scholar 

  6. Joseph Y. Halpern and Yoram Moses. A guide to completeness and complexity for modal logics of knowledge and belief. Artificial Intelligence, 54:319–379, 1992.

    Article  Google Scholar 

  7. Roger J. Hindley and Jonathan R. Seldin. Introduction to Combinators and Lambda Calculus. Cambridge University Press, 1986.

    Google Scholar 

  8. Jörg Hudelmaier. An O(nlog n)-space decision procedure for intuitionistic propositional logic. Journal of Logic and Computation, 3(1):63–75, 1993.

    Google Scholar 

  9. Richard E. Ladner. The computational complexity of provability in systems of modal propositional logic. SIAM journal on computing, 6(3):467–480, 1977.

    Article  Google Scholar 

  10. Nicholas Rescher and Alasdair Urquhart. Temporal Logic. Springer, 1971.

    Google Scholar 

  11. Dan Sahlin, Torkel Franzén, and Seif Haridi. An intuitionistic predicate logic theorem prover. Journal of Logic and Computation, 2(5):619–656, 1992.

    Google Scholar 

  12. Michael Seyfried. A sequent calculus for proof search in the (→, ∧)-fragment of intuitionistic logic. Technical notes, 1994.

    Google Scholar 

  13. Tanel Tammet. Proof search strategies in linear logic. Programming Methodology Group report 70, Department of Computer Sciences, Chalmers University of Technology, Göteborg, Sweden, 1993.

    Google Scholar 

  14. Heinrich Zimmermann. A directed tree calculus for minimal tense logic. Diploma thesis, IAM, University of Bern, Switzerland, 1994.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institut für Informatik und angewandte Mathematik, Universität Bern, Switzerland

    Alain Heuerding, Gerhard Jäger, Stefan Schwendimann & Michael Seyfried

Authors
  1. Alain Heuerding
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Gerhard Jäger
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Stefan Schwendimann
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Michael Seyfried
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Peter Baumgartner Reiner Hähnle Joachim Possega

Rights and permissions

Reprints and permissions

Copyright information

© 1995 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Heuerding, A., Jäger, G., Schwendimann, S., Seyfried, M. (1995). Propositional logics on the computer. In: Baumgartner, P., Hähnle, R., Possega, J. (eds) Theorem Proving with Analytic Tableaux and Related Methods. TABLEAUX 1995. Lecture Notes in Computer Science, vol 918. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-59338-1_44

Download citation

  • DOI: https://doi.org/10.1007/3-540-59338-1_44

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-59338-6

  • Online ISBN: 978-3-540-49235-1

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation