Journal of Symbolic Logic 67 (1):35-60 (2002)
|Abstract||The logical flow graphs of sequent calculus proofs might contain oriented cycles. For the predicate calculus the elimination of cycles might be non-elementary and this was shown in [Car96]. For the propositional calculus, we prove that if a proof of k lines contains n cycles then there exists an acyclic proof with O(k n+l ) lines. In particular, there is a polynomial time algorithm which eliminates cycles from a proof. These results are motivated by the search for general methods on proving lower bounds on proof size and by the design of more efficient heuristic algorithms for proof search|
|Keywords||No keywords specified (fix it)|
|Categories||categorize this paper)|
|Through your library||Configure|
Similar books and articles
Andrzej Wiśniewski (2004). Socratic Proofs. Journal of Philosophical Logic 33 (3):299-326.
Jan Krajíček (2004). Implicit Proofs. Journal of Symbolic Logic 69 (2):387 - 397.
Philippe De Groote & François Lamarche (2002). Classical Non-Associative Lambek Calculus. Studia Logica 71 (3):355 - 388.
Philippe de Groote & François Lamarche (2002). Classical Non-Associative Lambek Calculus. Studia Logica 71 (3):355-388.
Jan Krajíček (1997). Interpolation Theorems, Lower Bounds for Proof Systems, and Independence Results for Bounded Arithmetic. Journal of Symbolic Logic 62 (2):457-486.
Michael Alekhnovich, Sam Buss, Shlomo Moran & Toniann Pitassi (2001). Minimum Propositional Proof Length is NP-Hard to Linearly Approximate. Journal of Symbolic Logic 66 (1):171-191.
Erik Aarts (1994). Proving Theorems of the Second Order Lambek Calculus in Polynomial Time. Studia Logica 53 (3):373 - 387.
Maria Luisa Bonet & Samuel R. Buss (1993). The Deduction Rule and Linear and Near-Linear Proof Simulations. Journal of Symbolic Logic 58 (2):688-709.
Sorry, there are not enough data points to plot this chart.
Added to index2009-01-28
Total downloads1 ( #291,125 of 722,764 )
Recent downloads (6 months)0
How can I increase my downloads?