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