Towards a clausal analysis of cut-elimination

DOI10.1016/J.JSC.2003.10.005zbMath1125.03013OpenAlexW1995025865MaRDI QIDQ2457341

Matthias Baaz, Alexander Leitsch

Publication date: 23 October 2007

Published in: Journal of Symbolic Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.jsc.2003.10.005

zbMATH Keywords

resolutioncut-eliminationclause terms

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30) Mechanization of proofs and logical operations (03B35) Cut-elimination and normal-form theorems (03F05) Complexity of proofs (03F20)

Related Items (9)

Cut-Elimination and Proof Schemata ⋮ Extraction of expansion trees ⋮ CERES: An analysis of Fürstenberg's proof of the infinity of primes ⋮ Physics and proof theory ⋮ Cut-elimination: syntax and semantics ⋮ Proof Transformations and Structural Invariance ⋮ System Description: The Proof Transformation System CERES ⋮ Extension without cut ⋮ A Clausal Approach to Proof Analysis in Second-Order Logic

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Cut normal forms and proof complexity
• Untersuchungen über das logische Schliessen. II
• Generalizing theorems in real closed fields
• Herbrand-Analysen zweier Beweise des Satzes von Roth: Polynomiale Anzahlschranken
• A Machine-Oriented Logic Based on the Resolution Principle
• Cut-elimination and redundancy-elimination by resolution
• Interpolation theorems for intuitionistic predicate logic

This page was built for publication: Towards a clausal analysis of cut-elimination