Extraction of expansion trees
DOI10.1007/S10817-018-9453-9zbMATH Open1468.68296OpenAlexW2794392750WikidataQ92311822 ScholiaQ92311822MaRDI QIDQ670704FDOQ670704
Authors: Alexander Leitsch, Anela Lolic 
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
Recommendations
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)
Cites Work
- System description: GAPT 2.0
- Topological dynamics and combinatorial number theory
- Untersuchungen über das logische Schliessen. II
- Title not available (Why is that?)
- A compact representation of proofs
- On the Infinitude of Primes
- Refined program extraction from classical proofs
- ÜBER EINE BISHER NOCH NICHT BENÜTZTE ERWEITERUNG DES FINITEN STANDPUNKTES
- Title not available (Why is that?)
- Title not available (Why is that?)
- Methods of cut-elimination
- Herbrand Sequent Extraction
- Cut-elimination: syntax and semantics
- Towards a clausal analysis of cut-elimination
- Understanding Resolution Proofs through Herbrand’s Theorem
- Expansion trees with cut
- Logic for Programming, Artificial Intelligence, and Reasoning
- Proof Transformation by CERES
- Cut-elimination and redundancy-elimination by resolution
- CERES in higher-order logic
- Program extraction from normalization proofs
Cited In (5)
Uses Software
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)
