Herbrand Sequent Extraction

DOI10.1007/978-3-540-85110-3_38zbMath1166.68347MaRDI 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

03B35: Mechanization of proofs and logical operations

03F07: Structure of proofs

Related Items

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

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