Interpolants, cut elimination and flow graphs for the propositional calculus
DOI10.1016/S0168-0072(96)00019-XzbMATH Open0873.03050OpenAlexW2158086914MaRDI QIDQ674415FDOQ674415
Authors: Juan-Miguel Gracia 
Publication date: 26 October 1997
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(96)00019-x
Recommendations
- Streams and strings in formal proofs.
- Making proofs without Modus Ponens: An introduction to the combinatorics and complexity of cut elimination
- The cost of a cycle is a square
- scientific article; zbMATH DE number 1342249
- scientific article; zbMATH DE number 1748575
- Duplication of directed graphs and exponential blow up of proofs
- Gentzen's second consistency proof and strong cut-elimination
- Turning cycles into spirals
- Gentzen systems, resolution, and literal trees
- Logical structures and genus of proofs
interpolationcut eliminationsequent calculuslogical flow graphspropositional calculussize of interpolants
Cut-elimination and normal-form theorems (03F05) Structure of proofs (03F07) Complexity of proofs (03F20)
Cites Work
- Title not available (Why is that?)
- Title not available (Why is that?)
- Linear logic
- The relative efficiency of propositional proof systems
- Title not available (Why is that?)
- The number of proof lines and the size of proofs in first order logic
- A unification-theoretic method for investigating the \(k\)-provability problem
- Some Results on the Length of Proofs
- Title not available (Why is that?)
- Complexity of the realization of a linear function in the class of \(\Pi\)-circuits
- Title not available (Why is that?)
- The undecidability of \(k\)-provability
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- The Universe of Set Theory
- Interpolants, cut elimination and flow graphs for the propositional calculus
Cited In (18)
- Logical structures and genus of proofs
- Simulating non-prenex cuts in quantified propositional calculus
- Turning cycles into spirals
- A new mapping between combinatorial proofs and sequent calculus proofs read out from logical flow graphs
- Models of deduction
- Describing proofs by short tautologies
- Streams and strings in formal proofs.
- Craig interpolation in the presence of unreliable connectives
- Partition-based logical reasoning for first-order and propositional theories
- Identity of Proofs Based on Normalization and Generality
- Computing interpolants in implicational logics
- Cycling in proofs and feasibility
- Title not available (Why is that?)
- Making proofs without Modus Ponens: An introduction to the combinatorics and complexity of cut elimination
- The cost of a cycle is a square
- Asymptotic cyclic expansion and bridge groups of formal proofs
- Combinatorial flows as bicolored atomic flows
- Interpolants, cut elimination and flow graphs for the propositional calculus
This page was built for publication: Interpolants, cut elimination and flow graphs for the propositional calculus
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q674415)
