The cost of a cycle is a square
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 | ||||||||||
| Options |
|
|||||||||
Download options| PhilPapers Archive |
Upload a copy of this paper Check publisher's policy on self-archival Papers currently archived: 5,705 |
| External links |
  Try with proxy. |
| Through your library | Configure |
Similar books and articlesAndrzej 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.
Analytics
Monthly downloads
Sorry, there are not enough data points to plot this chart.
|
Added to index2009-01-28Total downloads1 ( #274,982 of 549,196 )Recent downloads (6 months)0How can I increase my downloads? |
My notes
Discussion
