Turning cycles into spirals

DOI10.1016/S0168-0072(98)00031-1MaRDI QIDQ1295442zbMATH OpenOpenAlexFDO

Authors V. Pereyra, Alessandra Carbone

Publication date 28 October 1999

Published in Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/s0168-0072(98)00031-1

zbMATH Keywords

cycles in proofslogical flow graphs

Mathematics Subject Classification ID

Structure of proofs (03F07) Complexity of proofs (03F20)

Review text

``Cycles in the title refers to those in logical flow graphs, a device \textit{S. R. Buss} introduced to analyze the LK proofs [Ann. Pure Appl. Log. 53, 75-102 (1991; Zbl 0749.03039)]. Such cycles make understanding the structure of a proof difficult. To avoid them, the author introduces a new calculus ALK [= Acyclic LK], which is obtained from LK by modifying rules, \(\exists\to\), \(\to\forall\), and Cut. In particular, Cut is allowed only when its Cut formula has a decent history in that Contractions in its logical paths must have the disjunction property. The author shows that ALK, indeed, avoids cycles, and those in LK become spirals in ALK. And, an LK proof of \(n\) lines can be turned into an ALK proof of \(\exp(\exp({\mathcal O}(n)))\) lines. [Here, \(\exp(x)\) means \(2^x\).] An ALK proof becomes an LK proof when necessary Contractions are added.

Recommendations

• The cost of a cycle is a square
• Removing cycles from proofs
• Duplication of directed graphs and exponential blow up of proofs
• Circular (yet sound) proofs

Cites work

• Bounds for proof-search and speed-up in the predicate calculus
• Cycling in proofs and feasibility
• Don't eliminate cut
• Existence and feasibility in arithmetic
• scientific article; zbMATH DE number 3687363 (Why is no real title available?)
• scientific article; zbMATH DE number 3313427 (Why is no real title available?)
• Interpolants, cut elimination and flow graphs for the propositional calculus
• Linear logic
• Looking from the inside and from the outside
• Lower bounds for increasing complexity of derivations after cut elimination
• Making proofs without Modus Ponens: An introduction to the combinatorics and complexity of cut elimination
• The undecidability of k-provability
• The Universe of Set Theory

Cited in

(7)

• On the decision problem for MELL
• Streams and strings in formal proofs.
• The cost of a cycle is a square
• Cycling in proofs and feasibility
• Combinatorial flows as bicolored atomic flows
• Interpolants, cut elimination and flow graphs for the propositional calculus
• On the form of witness terms

This page was built for publication: Turning cycles into spirals

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1295442)