Interpolants, cut elimination and flow graphs for the propositional calculus

DOI10.1016/S0168-0072(96)00019-XMaRDI QIDQ674415zbMATH OpenOpenAlexFDO

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

zbMATH Keywords

interpolationcut eliminationsequent calculuslogical flow graphspropositional calculussize of interpolants

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) Structure of proofs (03F07) Complexity of proofs (03F20)

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

Cites work

• scientific article; zbMATH DE number 3954886 (Why is no real title available?)
• scientific article; zbMATH DE number 4033740 (Why is no real title available?)
• scientific article; zbMATH DE number 3687363 (Why is no real title available?)
• scientific article; zbMATH DE number 65760 (Why is no real title available?)
• scientific article; zbMATH DE number 726524 (Why is no real title available?)
• scientific article; zbMATH DE number 1142303 (Why is no real title available?)
• scientific article; zbMATH DE number 910750 (Why is no real title available?)
• scientific article; zbMATH DE number 3073037 (Why is no real title available?)
• A unification-theoretic method for investigating the \(k\)-provability problem
• Complexity of the realization of a linear function in the class of -circuits
• Interpolants, cut elimination and flow graphs for the propositional calculus
• Linear logic
• Some Results on the Length of Proofs
• The Universe of Set Theory
• The number of proof lines and the size of proofs in first order logic
• The relative efficiency of propositional proof systems
• The undecidability of k-provability

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
• Describing proofs by short tautologies
• Models of deduction
• 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
• scientific article; zbMATH DE number 1507229 (Why is no real title available?)
• 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)