Cut-elimination and redundancy-elimination by resolution
From MaRDI portal
Publication:5927981
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
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