Lemmas: generation, selection, application

DOI10.1007/978-3-031-43513-3_9MaRDI QIDQ6541149

Christoph Wernhard, Zsolt Zombori, Wolfgang Bibel, Michael G. Rawson

Publication date: 17 May 2024

Mathematics Subject Classification ID

Could not fetch data.

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Learning-assisted theorem proving with millions of lemmas
• A curious inference
• A Prolog technology theorem prover: Implementation by an extended Prolog compiler
• SETHEO: A high-performance theorem prover
• In memoriam Carew Arthur Meredith (1904-1976)
• The resonance strategy
• Controlled integration of the cut rule into connection tableau calculi
• Upside-down meta-interpretation of the model elimination theorem-proving procedure for deduction and abduction
• The power of combining resonance with heat
• IeanCOP: lean connection-based theorem proving
• The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0
• TacticToe: learning to prove with tactics
• Learning from Łukasiewicz and Meredith: investigations into proof structures
• \textsf{lazyCoP}: lazy paramodulation meets neurally guided search
• The On-Line Encyclopedia of Integer Sequences
• Guiding inferences in connection tableau by recurrent neural networks
• First neural conjecturing datasets and experiments
• Faster, higher, stronger: E 2.3
• Machine learning for first-order theorem proving
• ENIGMA: efficient learning-based inference guiding machine
• On the generation of quantified lemmas
• Notes on the axiomatics of the propositional calculus
• Resolution theorem proving
• Tableaux and related methods
• Towards Algorithmic Cut-Introduction
• SWI-Prolog
• Lemmatization for Stronger Reasoning in Large Theories
• Atomic Cut Introduction by Resolution: Proof Structuring and Compression
• Cooperating Proof Attempts
• Principal type-schemes and condensed detachment
• MaLARea SG1 - Machine Learner for Automated Reasoning with Semantic Guidance
• Restricting backtracking in connection calculi
• Deep Network Guided Proof Search
• From Schütte’s Formal Systems to Modern Automated Deduction
• Machine Learning for Automated Theorem Proving: Learning to Solve SAT and QSAT
• Prolog Technology Reinforcement Learning Prover
• Hyper tableaux
• A legacy recalled and a tradition continued
• Finding shortest proofs: An application of linked inference rules
• Conquering the Meredith single axiom
• Missing proofs found
• Automated reasoning contributes to mathematics and logic
• Who finds the short proof?

Related Items (2)

Range-restricted and Horn interpolation through clausal tableaux ⋮ Investigations into proof structures

This page was built for publication: Lemmas: generation, selection, application

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