Cut-elimination and redundancy-elimination by resolution

DOI10.1006/jsco.1999.0359zbMath0976.03059OpenAlexW2077585224MaRDI QIDQ5927981

Matthias Baaz, Alexander Leitsch

Publication date: 19 March 2001

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

Full work available at URL: https://semanticscholar.org/paper/8cd7908da4d0670f34baa3a47e18a9d91c475240

zbMATH Keywords

classical predicate calculuscut-elimination procedurehyperexponential speed-upresolution refutation

Mathematics Subject Classification ID

Classical first-order logic (03B10) Mechanization of proofs and logical operations (03B35) Cut-elimination and normal-form theorems (03F05)

Related Items

Ceres in intuitionistic logic ⋮ On the complexity of proof deskolemization ⋮ Cut-Elimination and Proof Schemata ⋮ Schematic refutations of formula schemata ⋮ Unnamed Item ⋮ Towards a clausal analysis of cut-elimination ⋮ Sufficient conditions for cut elimination with complexity analysis ⋮ Extraction of expansion trees ⋮ CERES: An analysis of Fürstenberg's proof of the infinity of primes ⋮ Herbrand's theorem as higher order recursion ⋮ Cut-elimination: syntax and semantics ⋮ Proof Transformations and Structural Invariance ⋮ Herbrand's theorem and term induction ⋮ System Description: The Proof Transformation System CERES ⋮ On the form of witness terms ⋮ CERES in higher-order logic ⋮ Corrected upper bounds for free-cut elimination ⋮ A Clausal Approach to Proof Analysis in Second-Order Logic ⋮ Towards an algorithmic construction of cut-elimination procedures ⋮ Schematic Cut Elimination and the Ordered Pigeonhole Principle ⋮ System Description: GAPT 2.0 ⋮ Describing proofs by short tautologies ⋮ Expansion trees with cut ⋮ Herbrand Sequent Extraction ⋮ Book review of: Matthias Baaz and Alexander Leitsch, Methods of cut-elimination ⋮ CUT ELIMINATION AND NORMALIZATION FOR GENERALIZED SINGLE AND MULTI-CONCLUSION SEQUENT AND NATURAL DEDUCTION CALCULI

Cites Work

• Proof theory. 2nd ed
• Complexity of resolution proofs and function introduction
• Cut normal forms and proof complexity
• Untersuchungen über das logische Schliessen. II
• Herbrand-Analysen zweier Beweise des Satzes von Roth: Polynomiale Anzahlschranken
• Two Applications of Logic to Mathematics
• Lower Bounds on Herbrand's Theorem
• A Machine-Oriented Logic Based on the Resolution Principle
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item