Extraction of expansion trees

DOI10.1007/S10817-018-9453-9zbMath1468.68296OpenAlexW2794392750WikidataQ92311822 ScholiaQ92311822MaRDI QIDQ670704

Anela Lolic, Alexander Leitsch

Publication date: 20 March 2019

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

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

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

Related Items (2)

On structures of regular standard contradictions in propositional logic ⋮ Unnamed Item

Uses Software

• CERES
• GAPT
• ProofTool

Cites Work

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

This page was built for publication: Extraction of expansion trees