Learning from Łukasiewicz and Meredith: investigations into proof structures
From MaRDI portal
Publication:2055843
DOI10.1007/978-3-030-79876-5_4OpenAlexW3157934215MaRDI QIDQ2055843
Christoph Wernhard, Wolfgang Bibel
Publication date: 1 December 2021
Full work available at URL: https://arxiv.org/abs/2104.13645
Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Related Items (1)
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Algorithmic introduction of quantified cuts
- Condensed detachment as a rule of inference
- Properties of substitutions and unifications
- In memoriam Carew Arthur Meredith (1904-1976)
- A simplified form of condensed detachment
- Machine learning guidance for connection tableaux
- Learning from Łukasiewicz and Meredith: investigations into proof structures
- Faster, higher, stronger: E 2.3
- Notes on the axiomatics of the propositional calculus
- Atomic Cut Introduction by Resolution: Proof Structuring and Compression
- Single Axioms and Axiom-Pairs for the Implicational Fragments of $$\mathbf {R}$$ R , R-Mingle, and Some Related Systems
- Grammar-Based Tree Compression
- Principal type-schemes and condensed detachment
- System Description: E- KRHyper
- Variations on the Common Subexpression Problem
- From Schütte’s Formal Systems to Modern Automated Deduction
- ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (System Description)
- A legacy recalled and a tradition continued
- Finding shortest proofs: An application of linked inference rules
- Missing proofs found
This page was built for publication: Learning from Łukasiewicz and Meredith: investigations into proof structures
