Extraction of expansion trees

DOI10.1007/S10817-018-9453-9MaRDI QIDQ670704zbMATH OpenOpenAlexWikidataFDO

Authors Alexander Leitsch, Anela Lolic

Publication date 20 March 2019

Published in Journal of Automated Reasoning (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/s10817-018-9453-9

zbMATH Keywords

cut-eliminationexpansion treeHerbrand sequentproof mining

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Cut-elimination and normal-form theorems (03F05) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15) Formalization of mathematics in connection with theorem provers (68V20)

Recommendations

• scientific article; zbMATH DE number 7178366
• Methods of cut-elimination
• A compact representation of proofs
• Logic for Programming, Artificial Intelligence, and Reasoning
• Proof Transformation by CERES

Cites work

• A compact representation of proofs
• CERES in higher-order logic
• Cut-elimination and redundancy-elimination by resolution
• Cut-elimination: syntax and semantics
• Expansion trees with cut
• Herbrand Sequent Extraction
• scientific article; zbMATH DE number 3871342 (Why is no real title available?)
• scientific article; zbMATH DE number 4033738 (Why is no real title available?)
• scientific article; zbMATH DE number 627412 (Why is no real title available?)
• Logic for Programming, Artificial Intelligence, and Reasoning
• Methods of cut-elimination
• On the Infinitude of Primes
• Program extraction from normalization proofs
• Proof Transformation by CERES
• Refined program extraction from classical proofs
• System description: GAPT 2.0
• Topological dynamics and combinatorial number theory
• Towards a clausal analysis of cut-elimination
• Understanding Resolution Proofs through Herbrand’s Theorem
• Untersuchungen über das logische Schliessen. II
• ÜBER EINE BISHER NOCH NICHT BENÜTZTE ERWEITERUNG DES FINITEN STANDPUNKTES

Cited in

(9)

• A compact representation of proofs
• TBA and tree expansion
• scientific article; zbMATH DE number 3871341 (Why is no real title available?)
• scientific article; zbMATH DE number 7447752 (Why is no real title available?)
• On structures of regular standard contradictions in propositional logic
• Efficient interpolation beyond cut-free proofs: admissible cuts and optimized extraction
• Extracting Herbrand systems from refutation schemata
• A simplified proof of the epsilon theorems
• Efficient interpolation beyond cut-free proofs

Describes a project that uses

Uses Software

• CERES
• GAPT
• ProofTool

This page was built for publication: Extraction of expansion trees

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