Herbrand Sequent Extraction

DOI10.1007/978-3-540-85110-3_38MaRDI QIDQ5505525zbMATH OpenOpenAlexFDO

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

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)

Recommendations

• System Description: The Proof Transformation System CERES
• Extracting Herbrand disjunctions by functional interpretation
• Herbrand's theorem as higher order recursion
• Herbrand-confluence
• Sequent forms of Herbrand theorem and their applications

Cites work

• CERES: An analysis of Fürstenberg's proof of the infinity of primes
• Cut normal forms and proof complexity
• Cut-elimination and redundancy-elimination by resolution
• Extracting Herbrand disjunctions by functional interpretation
• Herbrand Sequent Extraction
• Herbrand-Analysen zweier Beweise des Satzes von Roth: Polynomiale Anzahlschranken
• scientific article; zbMATH DE number 627412 (Why is no real title available?)
• scientific article; zbMATH DE number 3333259 (Why is no real title available?)
• Logic for Programming, Artificial Intelligence, and Reasoning
• Lower Bounds on Herbrand's Theorem
• Proof Transformation by CERES
• Proof Transformations and Structural Invariance
• The state of CASC

Cited in

(16)

• Herbrand's theorem as higher order recursion
• 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
• Information-Extraction Through Reduction Methods In Some Formal Systems
• scientific article; zbMATH DE number 1950249 (Why is no real title available?)
• 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
• Extracting Herbrand systems from refutation schemata
• Herbrand's theorem in inductive proofs
• CERES in higher-order logic

This page was built for publication: Herbrand Sequent Extraction

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5505525)