Journal of Symbolic Logic 67 (1):35-60 (2002)
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)|
References found in this work BETA
Interpolants, Cut Elimination and Flow Graphs for the Propositional Calculus.Alessandra Carbone - 1997 - Annals of Pure and Applied Logic 83 (3):249-299.
Bounds for Proof-Search and Speed-Up in the Predicate Calculus.Richard Statman - 1978 - Annals of Mathematical Logic 15 (3):225-287.
Duplication of Directed Graphs and Exponential Blow Up of Proofs.A. Carbone - 1999 - Annals of Pure and Applied Logic 100 (1-3):1-67.
Some Remarks on Lengths of Propositional Proofs.Samuel R. Buss - 1995 - Archive for Mathematical Logic 34 (6):377-394.
Citations of this work BETA
No citations found.
Similar books and articles
A Simple Proof of Completeness and Cut-Elimination for Propositional G¨ Odel Logic.Arnon Avron - unknown
The Deduction Rule and Linear and Near-Linear Proof Simulations.Maria Luisa Bonet & Samuel R. Buss - 1993 - Journal of Symbolic Logic 58 (2):688-709.
Proving Theorems of the Second Order Lambek Calculus in Polynomial Time.Erik Aarts - 1994 - Studia Logica 53 (3):373 - 387.
Minimum Propositional Proof Length is NP-Hard to Linearly Approximate.Michael Alekhnovich, Sam Buss, Shlomo Moran & Toniann Pitassi - 2001 - Journal of Symbolic Logic 66 (1):171-191.
Interpolation Theorems, Lower Bounds for Proof Systems, and Independence Results for Bounded Arithmetic.Jan Krajíček - 1997 - Journal of Symbolic Logic 62 (2):457-486.
Classical Non-Associative Lambek Calculus.de Groote Philippe & Lamarche François - 2002 - Studia Logica 71 (3):355-388.
Classical Non-Associative Lambek Calculus.Philippe De Groote & François Lamarche - 2002 - Studia Logica 71 (3):355 - 388.
Added to index2009-01-28
Total downloads12 ( #374,474 of 2,163,699 )
Recent downloads (6 months)1 ( #348,043 of 2,163,699 )
How can I increase my downloads?