Logic Journal of the IGPL 8 (6):733-750 (2000)
It has been maintained by Smullyan that the importance of cut-free proofs does not stem from cut elimination per se but rather from the fact that they satisfy the subformula property. In accordance with such a viewpoint in this paper we introduce analytic cut trees, a system from which cuts cannot be eliminated but satisfying the subformula property. Like tableaux analytic cut trees are a refutation system but unlike tableaux they have a single inference rule and several branch closure rules. The main advantage of analytic cut trees over tableaux is efficiency: while analytic cut trees can simulate tableaux with an increase in complexity by at most a constant factor, tableaux cannot polynomially simulate analytic cut trees. Indeed analytic cut trees are intrinsically more efficient than any cut-free system.
|Keywords||No keywords specified (fix it)|
|Categories||categorize this paper)|
References found in this work BETA
No references found.
Citations of this work BETA
No citations found.
Similar books and articles
The Contemporary Significance of Confucianism.Tang Yijie & Yan Xin - 2008 - Frontiers of Philosophy in China 3 (4):477-501.
Shifting Frames: From Divided to Distributed Psychologies of Scientific Agents.Peter J. Taylor - 1994 - PSA: Proceedings of the Biennial Meeting of the Philosophy of Science Association 1994:304-310.
Commodification or Compensation: A Reply to Ketchum.H. M. Malm - 1989 - Hypatia 4 (3):128-135.
A Novel Interpretation of Plato's Theory of Forms.P. X. Monaghan - 2010 - Metaphysica 11 (1):63-78.
Added to index2009-01-28
Total downloads269 ( #11,815 of 2,158,310 )
Recent downloads (6 months)14 ( #25,376 of 2,158,310 )
How can I increase my downloads?