Herbrand Sequent Extraction

DOI10.1007/978-3-540-85110-3_38zbMath1166.68347OpenAlexW2117600025MaRDI QIDQ5505525

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

Publication date: 27 January 2009

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: http://resolver.obvsg.at/urn:nbn:at:at-ubtuw:1-18086

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Structure of proofs (03F07)

Related Items (11)

Towards the Compression of First-Order Resolution Proofs by Lowering Unit Clauses ⋮ Implementation and Evaluation of Contextual Natural Deduction for Minimal Logic ⋮ Schematic refutations of formula schemata ⋮ On the elimination of quantifier-free cuts ⋮ Extraction of expansion trees ⋮ Physics and proof theory ⋮ System Description: The Proof Transformation System CERES ⋮ CERES in higher-order logic ⋮ Complexity of translations from resolution to sequent calculus ⋮ Herbrand Sequent Extraction ⋮ Inductive theorem proving based on tree grammars

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• CERES: An analysis of Fürstenberg's proof of the infinity of primes
• Cut normal forms and proof complexity
• Extracting Herbrand disjunctions by functional interpretation
• Herbrand-Analysen zweier Beweise des Satzes von Roth: Polynomiale Anzahlschranken
• Lower Bounds on Herbrand's Theorem
• Proof Transformations and Structural Invariance
• Herbrand Sequent Extraction
• Logic for Programming, Artificial Intelligence, and Reasoning
• Proof Transformation by CERES
• Cut-elimination and redundancy-elimination by resolution

This page was built for publication: Herbrand Sequent Extraction