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-eliminationproof miningexpansion treeHerbrand sequent

Mathematics Subject Classification ID

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

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

• 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?)
• 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
• 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

(5)

• scientific article; zbMATH DE number 7447752 (Why is no real title available?)
• TBA and tree expansion
• scientific article; zbMATH DE number 3871341 (Why is no real title available?)
• On structures of regular standard contradictions in propositional logic
• A compact representation of proofs

Describes a project that uses

Uses Software

• ProofTool
• GAPT
• CERES

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)