Learning from Łukasiewicz and Meredith: investigations into proof structures

DOI10.1007/978-3-030-79876-5_4OpenAlexW3157934215MaRDI QIDQ2055843FDOQ2055843

Authors: Christoph Wernhard, Wolfgang Bibel 

Publication date: 1 December 2021

Full work available at URL: https://arxiv.org/abs/2104.13645

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites Work

• Faster, higher, stronger: E 2.3
• System Description: E- KRHyper
• Variations on the Common Subexpression Problem
• Properties of substitutions and unifications
• Title not available (Why is that?)
• Title not available (Why is that?)
• Tableaux and related methods
• Title not available (Why is that?)
• Atomic cut introduction by resolution: proof structuring and compression
• Algorithmic introduction of quantified cuts
• Grammar-Based Tree Compression
• Notes on the axiomatics of the propositional calculus
• Title not available (Why is that?)
• Title not available (Why is that?)
• Principal type-schemes and condensed detachment
• Automated reasoning contributes to mathematics and logic
• A legacy recalled and a tradition continued
• ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (System Description)
• In memoriam Carew Arthur Meredith (1904-1976)
• Title not available (Why is that?)
• Condensed detachment as a rule of inference
• Title not available (Why is that?)
• Title not available (Why is that?)
• A simplified form of condensed detachment
• Machine learning guidance for connection tableaux
• Learning from Łukasiewicz and Meredith: investigations into proof structures
• Single Axioms and Axiom-Pairs for the Implicational Fragments of $$\mathbf {R}$$ R , R-Mingle, and Some Related Systems
• From Schütte’s Formal Systems to Modern Automated Deduction
• Finding shortest proofs: An application of linked inference rules
• Missing proofs found

Cited In (4)

• Learning from Łukasiewicz and Meredith: investigations into proof structures
• Investigations into proof structures
• Lemmas: generation, selection, application
• Range-restricted and Horn interpolation through clausal tableaux

This page was built for publication: Learning from Łukasiewicz and Meredith: investigations into proof structures

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