Streams and strings in formal proofs.

DOI10.1016/S0304-3975(01)00145-1zbMath1061.03059OpenAlexW2075407807WikidataQ57253071 ScholiaQ57253071MaRDI QIDQ1853510

Yanyan Li

Publication date: 21 January 2003

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/s0304-3975(01)00145-1

zbMATH Keywords

Proof complexityDirected graphsCut eliminationCycles in proofsDuplicationLogical flow graphsStructure of proofs

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) Grammars and rewriting systems (68Q42) Structure of proofs (03F07) Complexity of proofs (03F20)

Related Items

Logical structures and genus of proofs, Group cancellation and resolution

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Linear logic
• Interpolants, cut elimination and flow graphs for the propositional calculus
• The intractability of resolution
• Proof theory. 2nd ed
• Duplication of directed graphs and exponential blow up of proofs
• Lower bounds for increasing complexity of derivations after cut elimination
• The undecidability of \(k\)-provability
• Turning cycles into spirals
• Untersuchungen über das logische Schliessen. I
• Looking from the inside and from the outside
• Bounds for proof-search and speed-up in the predicate calculus
• Lower Bounds on Herbrand's Theorem
• Making proofs without Modus Ponens: An introduction to the combinatorics and complexity of cut elimination
• Cycling in proofs and feasibility
• Asymptotic cyclic expansion and bridge groups of formal proofs