Lemmas: generation, selection, application
From MaRDI portal
Publication:6541149
DOI10.1007/978-3-031-43513-3_9MaRDI QIDQ6541149FDOQ6541149
Authors: Michael G. Rawson, Christoph Wernhard, Zsolt Zombori, Wolfgang Bibel 
Publication date: 17 May 2024
Cites Work
- Faster, higher, stronger: E 2.3
- SWI-Prolog
- Resolution theorem proving
- A Prolog technology theorem prover: Implementation by an extended Prolog compiler
- SETHEO: A high-performance theorem prover
- Lemmatization for stronger reasoning in large theories
- MaLARea SG1 - Machine Learner for Automated Reasoning with Semantic Guidance
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Tableaux and related methods
- Title not available (Why is that?)
- Towards Algorithmic Cut-Introduction
- Atomic cut introduction by resolution: proof structuring and compression
- The On-Line Encyclopedia of Integer Sequences
- Title not available (Why is that?)
- Notes on the axiomatics of the propositional calculus
- Title not available (Why is that?)
- Title not available (Why is that?)
- Machine learning for first-order theorem proving
- Learning-assisted theorem proving with millions of lemmas
- Machine Learning for Automated Theorem Proving: Learning to Solve SAT and QSAT
- A curious inference
- Principal type-schemes and condensed detachment
- Upside-down meta-interpretation of the model elimination theorem-proving procedure for deduction and abduction
- Automated reasoning contributes to mathematics and logic
- The resonance strategy
- A legacy recalled and a tradition continued
- Conquering the Meredith single axiom
- The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0
- ENIGMA: efficient learning-based inference guiding machine
- Deep network guided proof search
- Hyper tableaux
- In memoriam Carew Arthur Meredith (1904-1976)
- Controlled integration of the cut rule into connection tableau calculi
- IeanCOP: lean connection-based theorem proving
- Title not available (Why is that?)
- \textsf{lazyCoP}: lazy paramodulation meets neurally guided search
- The power of combining resonance with heat
- First neural conjecturing datasets and experiments
- TacticToe: learning to prove with tactics
- Restricting backtracking in connection calculi
- Learning from Łukasiewicz and Meredith: investigations into proof structures
- From Schütte’s Formal Systems to Modern Automated Deduction
- Finding shortest proofs: An application of linked inference rules
- Missing proofs found
- Guiding inferences in connection tableau by recurrent neural networks
- Prolog Technology Reinforcement Learning Prover
- On the generation of quantified lemmas
- Title not available (Why is that?)
- Cooperating proof attempts
- Title not available (Why is that?)
- Who finds the short proof?
Cited In (2)
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)
