Turning cycles into spirals
type: Item
instance of: scholarly article
title: Turning cycles into spirals
zbMATH Open document ID: 0923.03066
DOI: 10.1016/S0168-0072(98)00031-1
author: V. Pereyra
published in: Annals of Pure and Applied Logic
publication date: 1999-10-28T00:00:00Z
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.
Mathematics Subject Classification ID: 03F07
Mathematics Subject Classification ID: 03F20
zbMATH DE Number: 1308113
zbMATH Keywords: cycles in proofs
zbMATH Keywords: logical flow graphs
MaRDI profile type: Publication
cites work: Don't eliminate cut
cites work: The undecidability of \(k\)-provability
cites work: Interpolants, cut elimination and flow graphs for the propositional calculus
cites work: Cycling in proofs and feasibility
cites work: Looking from the inside and from the outside
cites work: Making proofs without Modus Ponens: An introduction to the combinatorics and complexity of cut elimination
cites work: Q3882443
cites work: Linear logic
cites work: Lower bounds for increasing complexity of derivations after cut elimination
cites work: Existence and feasibility in arithmetic
cites work: Bounds for proof-search and speed-up in the predicate calculus
cites work: The Universe of Set Theory
cites work: Q5593816
full work available at URL: s0168-0072(98)00031-1
OpenAlex ID: W2014024837
description: scientific article; zbMATH DE number 1308113