Journal of Logic, Language and Information 1 (3):235-252 (1992)
|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.|
|Keywords||tableaux truth-tables computational complexity theorem-proving|
|Categories||categorize this paper)|
|Through your library||Configure|
Similar books and articles
Francis Jeffry Pelletier (1998). Automated Natural Deduction in Thinker. Studia Logica 60 (1):3-43.
Atocha Aliseda (2005). Lacunae, Empirical Progress and Semantic Tableaux. Poznan Studies in the Philosophy of the Sciences and the Humanities 83 (1):169-189.
Bernhard Beckert & Rajeev GorÉ (2001). Free-Variable Tableaux for Propositional Modal Logics. Studia Logica 69 (1):59-96.
André Vellino (1993). The Relative Complexity of Analytic Tableaux and SL-Resolution. Studia Logica 52 (2):323 - 337.
Noriko H. Arai, Toniann Pitassi & Alasdair Urquhart (2006). The Complexity of Analytic Tableaux. Journal of Symbolic Logic 71 (3):777 - 790.
Carlo Cellucci (2000). Analytic Cut Trees. Logic Journal of the IGPL 8:733-750.
Added to index2009-01-28
Total downloads5 ( #169,891 of 722,708 )
Recent downloads (6 months)1 ( #60,247 of 722,708 )
How can I increase my downloads?