A Clausal Approach to Proof Analysis in Second-Order Logic

DOI10.1007/978-3-540-92687-0_15zbMath1211.03018OpenAlexW1605178040MaRDI QIDQ3605531

Stefan Hetzl, Daniel Weller, Alexander Leitsch, Bruno Woltzenlogel Paleo

Publication date: 24 February 2009

Published in: Logical Foundations of Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-540-92687-0_15

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05)

Related Items (2)

System Description: The Proof Transformation System CERES ⋮ CERES in higher-order logic

Uses Software

• CERES

Cites Work

• Unnamed Item
• CERES in higher-order logic
• CERES: An analysis of Fürstenberg's proof of the infinity of primes
• A compact representation of proofs
• Cut normal forms and proof complexity
• Comparing approaches to resolution based higher-order theorem proving
• Towards a clausal analysis of cut-elimination
• Effective bounds from ineffective proofs in analysis: An application of functional interpretation and majorization
• A new deconstructive logic: linear logic
• Resolution in type theory
• Proof Transformation by CERES
• A formulation of the simple theory of types
• Proof theory
• Cut-elimination and redundancy-elimination by resolution

This page was built for publication: A Clausal Approach to Proof Analysis in Second-Order Logic