Abstract
We show that Smullyan's analytic tableaux cannot p-simulate the truth-tables. We identify the cause of this computational breakdown and relate it to an underlying semantic difficulty which is common to the whole tradition originating in Gentzen's sequent calculus, namely the dissonance between cut-free proofs and the Principle of Bivalence. Finally we discuss some ways in which this principle can be built into a tableau-like method without affecting its “analytic” nature.
This is a preview of subscription content, log in via an institution to check access.
Similar content being viewed by others
References
BethEvert W., 1955, “Semantic entailment and formal derivability,” Mededelingen der Koninklijke Nederlandse Akademie van Wetenschappen 18, 309–342.
BethEvert W., 1958, “On machines which prove theorems,” Simon Stevin Wissen Naturkundig Tijdschrift 32, 49–60.
BibelW., 1982. Automated Theorem Proving, Braunschweig: Vieweg.
CarnielliW.A., 1987, “Systematization of finite many-valued logics through the method of tableaux,” The Journal of Symbolic Logic 52, 473–493.
ChangC.L., 1970, “The unit proof and the input proof in theorem proving,” Journal of the Association for Computing Machinery 17, 698–707.
ChangC.L. and LeeR.C.T., 1973, Symbolic Logic and Mechanical Theorem Proving, Boston: Academic Press.
Cook, S.A. and Rechow, R., 1974, “On the length of proofs in the propositional calculus,” in pp. 135–148. Proceedings of the 6th Annual Symposium on the Theory of Computing.
CookS.A. and RechowR., 1979, “The relative efficiency of propositional proof systems,” The Journal of Symbolic Logic 44, 36–50.
D'Agostino, Marcello, 1990, “Investigations into the complexity of some propositional calculi,” PRG Technical Monographs 88, Oxford University Computing Laboratory.
D'Agostino, Marcello and Mondadori, Marco, 1992, “An improvement of analytic tableaux,” Extended abstract presented at the Workshop on Theorem Proving with Analytic Tableaux and Related Methods, Lautenbach 18–20 March 1992. Full version forthcoming.
DavisM. and PutmanH., 1960, “A computing procedure for quantification theory,” Journal of the Association for Computing Machinery 7, 201–215. Reprinted in Siegman and Wrightson (1983, pp. 125–139).
DavisM., LogemannG. and LovelandD., 1962, “A machine program for theorem proving,” Communications of the Association for Computing Machinery 5, 394–397. Reprinted in Siekman and Wrightson (1983, pp. 267–270).
DunhamBradford and WangHao, 1976, “Towards feasible solutions of the tautology problem,” Annals of Mathematical Logic 10, 117–154.
FittingMelvin, 1990, First-Order Logic and Automated Theorem Proving, Berlin: Springer-Verlag.
GallierJean H., 1986, Logic for Computer Science, New York: Harper & Row.
GentzenGerhard, 1935, “Untersuchungen uber das logische Schliessen,” Math. Zeitschrift 39, 176–210. English translation in Szabo (1969).
GirardI., 1987, Proof Theory and Logical Complexity, Napoli: Bibliopolis.
HaehnleReiner 1990, “Towards an efficient tableau proof procedure for multiple-valued logics,” in Proceedings Workshop on Computer Science Logic, Heidelberg: LNCS, Springer-Verlag.
Haehnle, Reiner, 1991, “Uniform notation of tableau rules for multiple-valued logics,” in Proceedings International Symposium on Multiple-Valued Logic, Victoria.
Haehnle, Reiner, 1992, “Tableaux-based theorem proving in multiple-valued logics,” Thesis, Institute for Logic, Complexity and Deduction Systems, Department of Computer Science, University of Karlsruhe, Germany.
Hintikka, Jaakko K.J., 1955, “Form and content in quatification theory,” Acta Philosophica Fennica, VIII.
JeffreyRichard C., 1967, Formal Logic: Its Scope and Limits, second edition. New York: McGraw-Hill Book Company. First edition 1967.
Mondadori, Marco, 1988a, “Classical analytical deduction,” Annali dell'Università di Ferrara; Sez. III; Discussion paper series 1, Università di Ferrara.
Mondadori, Marco, 1988b, “Classical analytical deduction, part II,” Annali dell'Università di Ferrara; Sez. III; Discussion paper series 5, Università di Ferrara.
Mondadori, Marco, 1989, “An improvement of Jeffrey's deductive trees,” Annali dell'Università di Ferrara; Sez. III; Discussion paper series 7, Università di Ferrara.
OppacherF. and SuenE., 1988, “HARP: A tableau-based theorem prover,” Journal of Automated Reasoning 4, 69–100.
SmullyanR., 1968a, First-Order Logic, Berlin: Springer.
SmullyanRaymond M., 1968b, “Analytic cut,” The Journal of Symbolic Logic 33, 560–564.
SiekmanJořg and WrightsonGraham (eds.), 1983, Automation of Reasoning, New York: Springer-Verlag.
SzaboM. ed., 1969, Collected Papers of Gerhard Gentzen, Amsterdam: North-Holland.
Urquhart, A., 1992, “Complexity of proofs in classical propositional logic,” pp. 596–608 in Logic from Computer Science, Y. Moschovakis, ed., Springer-Verlag.
WallenL.A., 1990, Automated Deduction in Non-Classical Logics, Cambridge, Mass.: The MIT Press.
Author information
Authors and Affiliations
Additional information
I am indebted to Marco Mondadori and Alasdair Urquhart for important suggestions. I wish also to thank Krysia Broda, Jeremy Pitt and an anonymous referee for helpful criticism.
Rights and permissions
About this article
Cite this article
D'Agostino, M. Are tableaux an improvement on truth-tables?. J Logic Lang Inf 1, 235–252 (1992). https://doi.org/10.1007/BF00156916
Received:
Accepted:
Issue Date:
DOI: https://doi.org/10.1007/BF00156916