Skip to main content
SpringerLink
Log in

Tableau Methods for Classical Propositional Logic

  • Chapter
Handbook of Tableau Methods

Abstract

Traditionally, a mathematical problem was considered ‘closed’ when an algorithm was found to solve it ‘in principle’. In this sense the deducibility problem of classical propositional logic was already ‘closed’ in the early 1920’s, when Wittgenstein and Post independently devised the well-known decision procedure based on the truth-tables. As usually happens this positive result ended up killing any theoretical interest in the subject. In contrast, first order logic was spared by a negative result. Its undecidability, established by Church and Turing in the 1930’s, made it an ‘intrinsically’ interesting subject forever. If no decision procedure can be found, that is all decision procedures have to be partial, the problem area is in no danger of saturation: it is always possible to find ‘better’ methods (at least for certain purposes).

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 169.00
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 219.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info
Hardcover Book
USD 219.99
Price excludes VAT (USA)
  • Durable hardcover edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. A. Avron. The semantics and proof theory of linear logic. Theoretical Computer Science, 57: 161–184, 1988.

    Google Scholar 

  2. E. W. Beth. Semantic entailment and formal derivability. Mededelingen der Koninklijke Nederlandse Akademie van Wetenschappen, 18: 309–342, 1955.

    Google Scholar 

  3. E. W. Beth. On machines which prove theorems. Simon Stevin Wissen Natur-kundig Tijdschrift, 32:49–60, 1958. Reprinted in [Siekmann and Wrightson, 1983 ], vol. 1, pages 79–90.

    Google Scholar 

  4. W. Bibel. Automated Theorem Proving. Vieweg, Braunschweig, 1982.

    Book  Google Scholar 

  5. R. Blanché. La logique et son histoire. Armand Colin, Paris, 1970.

    Google Scholar 

  6. I. M. Bochensky. A History of Formal Logic. University of Notre Dame, Notre Dame (Indiana ), 1961.

    Google Scholar 

  7. G. Boolos. Don’t eliminate cut. Journal of Philosophical Logic, 7: 373–378, 1984.

    Google Scholar 

  8. K. Broda. The application of semantic tableaux with unification to automated deduction. Ph.D thesis. Technical report, Department of Computing, Imperial College, 1992.

    Google Scholar 

  9. K. Broda, M. Finger and A. Russo. LDS-Natural deduction for substructural logics. Technical report DOC97–11. Imperial College, Department of Computing, 1997. Short version presented at WOLLIC 96, Journal of the IGPL,4:486–489.

    Google Scholar 

  10. S. R. Buss. Polynomial size proofs of the pigeon-hole principle. The Journal of Symbolic Logic, 52: 916–927, 1987.

    Article  Google Scholar 

  11. Cellucci, to appear] C. Cellucci. Analytic cut trees. To appear in the Journal of the IGPL.

    Google Scholar 

  12. Cellucci, 1987] C. Cellucci. Using full first order logic as a programming language. In Rendiconti del Seminario Matematico Università e Politecnico di Torino. Fascicolo Speciale 1987,pages 115–152, 1987. Proceedings of the conference on `Logic and Computer Science: New Trends and Applications’.

    Google Scholar 

  13. C. Cellucci. Existential instantiation and normalization in sequent natural deduction. Annals of Pure and Applied Logic, 58: 111–148, 1992.

    Article  Google Scholar 

  14. C. L. Chang. The unit proof and the input proof in theorem proving. Journal of the Association for Computing Machinery, 17: 698–707, 1970.

    Article  Google Scholar 

  15. C.L Chang and R. C. T. Lee. Symbolic Logic and Mechanical Theorem Proving. Academic Press, Boston, 1973.

    Google Scholar 

  16. S. A. Cook. The complexity of theorem proving procedures. In Proceedings of the 3rd Annual Symposium on the Theory of Computing, 1971.

    Google Scholar 

  17. S. A. Cook and R. Reckhow. On the length of proofs in the propositional calculus. In Proceedings of the 6th Annual Symposium on the Theory of Computing, pages 135–148, 1974.

    Google Scholar 

  18. S. A. Cook and R. Reckhow. The relative efficiency of propositional proof systems. The Journal of Symbolic Logic, 44: 36–50, 1979.

    Article  Google Scholar 

  19. M. D’Agostino. Investigations into the complexity of some propositional calculi. PRG Technical Monographs 88, Oxford University Computing Laboratory, 1990.

    Google Scholar 

  20. Are tableaux an improvement on truth-tables? Journal of Logic, Language and Information, 1: 235–252, 1992.

    Google Scholar 

  21. M. D’Agostino and D. Gabbay. A generalisation of analytic deduction via labelled deductive systems. Part 1: basic substructural logics. Journal of Automated Reasoning, 13: 243–281, 1994.

    Article  Google Scholar 

  22. M. D’Agostino and M. Mondadori. The taming of the cut. Journal of Logic and Computation, 4: 285–319, 1994.

    Article  Google Scholar 

  23. M. Davis. The prehistory and early history of automated deduction. In [Siekmann and Wrightson, 1983], pages 1–28. 1983.

    Google Scholar 

  24. M. Davis, G. Logemann, and D. Loveland. A machine program for theorem proving. Communications of the Association for Computing Machinery,5:394–397, 1962. Reprinted in [Siekmann and Wrightson, 1983], pp. 267–270.

    Google Scholar 

  25. M. Davis and H. Putnam. A computing procedure for quantification theory. Journal of the Association for Computing Machinery, 7:201–215, 1960. Reprinted in [Siekmann and Wrightson, 1983 ], pp. 125–139.

    Google Scholar 

  26. M. Dummett. Truth and other Enigmas. Duckworth, London, 1978.

    Google Scholar 

  27. B. Dunham and H. Wang. Towards feasible solutions of the tautology problem. Annals of Mathematical Logic, 10: 117–154, 1976.

    Article  Google Scholar 

  28. M. Fitting. First-Order Logic and Automated Theorem Proving. Springer-Verlag, Berlin, 1996. First edition, 1990.

    Google Scholar 

  29. D. M. Gabbay. Labelled Deductive Systems, Volume 1 - Foundations. Oxford University Press, 1996.

    Google Scholar 

  30. J. H. Gallier. Logic for Computer Science. Harper & Row, New York, 1986.

    Google Scholar 

  31. M. R. Garey and D. S. Johnson. Computers and Intractability. A Guide to the theory of NP-Completeness. W. H. Freeman & Co., San Francisco, 1979.

    Google Scholar 

  32. G. Gentzen. Unstersuchungen über das logische Schliessen. Math. Zeitschrift, 39:176–210, 1935. English translation in [Szabo, 1969 ].

    Google Scholar 

  33. J. Y. Girard. Proof Theory and Logical Complexity. Bibliopolis, Napoli, 1987.

    Google Scholar 

  34. J.-Y. Girard, Y. Lafont and P. Taylor. Proofs and Types. Cambridge Tracts in Theoretical Computer Science, Cambridge University Press, 1989.

    Google Scholar 

  35. R. Hähnle. Tableau-Based Theorem-Proving in Multiple-Valued Logics. PhD thesis, Department of Computer Science, University of Karlsruhe, 1992.

    Google Scholar 

  36. A. Heyting. Intuitionism. North-Holland, Amsterdam, 1956.

    Google Scholar 

  37. R. C. Jeffrey. Formal Logic: its Scope and Limits. McGraw-Hill Book Company, New York, second edition, 1981. first edition 1967.

    Google Scholar 

  38. S. C. Kleene. Mathematical Logic. John Wiley & Sons, Inc., New York, 1967.

    Google Scholar 

  39. R Letz. On the Polynomial Transparency of Resolution. In Proceedings of the 13th International Joint Conference on Artificial Intelligence(IJCAI), Chambery, pp. 123–129, 1993.

    Google Scholar 

  40. R Letz, K. Mayr and C. Goller. Controlled integration of the cut rule into connection tableaux calculi. Journal of Automated Reasoning, 13: 297–337, 1994.

    Article  Google Scholar 

  41. D. W. Loveland. Automated Theorem Proving: A Logical Basis. North Holland, 1978.

    Google Scholar 

  42. V. A. Matulis. Two versions of classical computation of predicates without structural rules. Soviet Mathematics, 3: 1770–1773, 1962.

    Google Scholar 

  43. M. Mondadori. Classical analytical deduction. Annali dell’Università di Ferrara; Sez. III; Discussion paper 1, Università di Ferrara, 1988.

    Google Scholar 

  44. M. Mondadori. Classical analytical deduction, part II. Annali dell’Università di Ferrara; Sez. III; Discussion paper 5, Università di Ferrara, 1988.

    Google Scholar 

  45. N. V. Murray and E. Rosenthal. On the computational intractability of analytic tableau methods. Bulletin of the IGPL, 1994.

    Google Scholar 

  46. D. Prawitz. Natural Deduction. A Proof-Theoretical Study. Almqvist & Wilksell, Uppsala, 1965.

    Google Scholar 

  47. Prawitz, 1971] D. Prawitz. Ideas and results in proof theory. In Proceedings of the II Scandinavian Logic Symposium,pages 235–308, Amsterdam, 1971. North-Holland.

    Google Scholar 

  48. D. Prawitz. Comments on Gentzen-type procedures and the classical notion of truth. In A. Dold and B. Eckman, editors, ISILC Proof Theory Symposium. Lecture Notes in Mathematics, 500, pages 290–319, Springer. Berlin, 1974.

    Google Scholar 

  49. D. Prawitz. Proofs and the meaning and completeness of the logical constants. In J. Hintikka, I. Niinduoto, and E. Saarinen, editors, Essays on Mathematical and Philosphical Logic, pages 25–40. Reidel, Dordrecht, 1978.

    Google Scholar 

  50. J. A. Robinson. A machine-oriented logic based on the resolution principle. Journal of the Association for Computing Machinery, 12: 23–41, 1965.

    Article  Google Scholar 

  51. P. Schroeder-Heister. Frege and the resolution calculus. History and Philosophy of Logic, 18: 95–108, 1997.

    Article  Google Scholar 

  52. D. Scott. Outline of a mathematical theory of computation. PRG Technical Monograph 2, Oxford University Computing Laboratory, Programming Research Group, 1970. Revised and expanded version of a paper under the same tide in the Proceedings of the Fourth Annual Princeton Conference on Information Sciences and System, 1970.

    Google Scholar 

  53. D. Scott. Notes on the formalization of logic. Study aids monographs, n. 3, University of Oxford, Subfaculty of Philosophy, 1981. Compiled by Dana Scott with the aid of David Bostock, Graeme Forbes, Daniel Isaacson and Gören Sundholm.

    Google Scholar 

  54. W. Sieg. Mechanism and search. aspects of proof theory. Technical report, AILA preprint, 1993.

    Google Scholar 

  55. J. Siekmann and G. Wrightson, editors. Automation of Reasoning. Springer-Verlag, New York, 1983.

    Google Scholar 

  56. R. Smullyan. First-Order Logic. Springer, Berlin, 1968.

    Book  Google Scholar 

  57. R. M. Smullyan. Uniform Gentzen systems. The Journal of Symbolic Logic, 33: 549–559, 1968.

    Article  Google Scholar 

  58. R. Statman. Bounds for proof-search and speed-up in the predicate calculus. Annals of Mathematical Logic, 15: 225–287, 1978.

    Article  Google Scholar 

  59. R. Statman. Herbrand’s theorem and Gentzen’s notion of a direct proof. In J. Barwise, editor, Handbook of Mathematical Logic, pages 897–912. North-Holland, Amsterdam, 1977.

    Chapter  Google Scholar 

  60. L. Stockmeyer. Classifying the computational complexity of problems. The Journal of Symbolic Logic, 52: 1–43, 1987.

    Article  Google Scholar 

  61. G. Sundholm. Systems of deduction. In D. Gabbay and R Guenthner, editors, Handbook of Philosophical Logic, volume I, chapter I.2, pages 133–188. Reidel, Dordrecht, 1983.

    Google Scholar 

  62. M. Szabo, editor. The Collected Papers of Gerhard Gentzen. North-Holland, Amsterdam, 1969.

    Google Scholar 

  63. N. Tennant. Natural Logic. Edimburgh University Press, Edinburgh, 1978.

    Google Scholar 

  64. R. B. Thistlewaite, M. A. McRobbie and B. K. Meyer. Automated Theorem Proving in Non Classical Logics. Pitman, 1988.

    Google Scholar 

  65. I. Thomas, editor. Greek Mathematics, volume 2. William Heinemann and Harvard University Press, London and Cambridge, Mass., 1941.

    Google Scholar 

  66. A. Urquhart. Complexity of proofs in classical propositional logic. In Y. Moschovakis, editor, Logic from Computer Science, pages 596–608. Springer-Verlag, 1992.

    Google Scholar 

  67. A. Urquhart. The complexity of propositional proofs. The Bulletin of Symbolic Logic, 1: 425–467, 1995.

    Article  Google Scholar 

  68. A. Vellino. The Complexity of Automated Reasoning. PhD thesis, University of Toronto, 1989.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Dipartimento di Scienze Umane, Università di Ferrara, Italy

    Marcello D’Agostino

Authors
  1. Marcello D’Agostino
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Università di Ferrara, Ferrara, Italy

    Marcello D’Agostino

  2. King’s College, London, UK

    Dov M. Gabbay

  3. Universität Karlsruhe, Germany

    Reiner Hähnle

  4. Research Centre, Deutsche Telekom AG, Darmstadt, Germany

    Joachim Posegga

Rights and permissions

Reprints and permissions

Copyright information

© 1999 Springer Science+Business Media Dordrecht

About this chapter

Cite this chapter

D’Agostino, M. (1999). Tableau Methods for Classical Propositional Logic. In: D’Agostino, M., Gabbay, D.M., Hähnle, R., Posegga, J. (eds) Handbook of Tableau Methods. Springer, Dordrecht. https://doi.org/10.1007/978-94-017-1754-0_2

Download citation

  • DOI: https://doi.org/10.1007/978-94-017-1754-0_2

  • Publisher Name: Springer, Dordrecht

  • Print ISBN: 978-90-481-5184-4

  • Online ISBN: 978-94-017-1754-0

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation