---
title: "Reinforcement Learning of Theorem Proving — Kaliszyk 2018"
description: "The paper asks whether a first-order theorem prover can learn its proof-search strategy from… 44 references, cited by 35 papers here."
authors: ["Cezary Kaliszyk", "Josef Urban", "Henryk Michalewski", "Mirek Olšák"]
year: 2018
venue: "arXiv:1805.07563"
source: "https://arxiv.org/abs/1805.07563"
doi: "10.48550/arxiv.1805.07563"
arxiv: "1805.07563"
licence: "arXiv — non-exclusive licence to distribute"
licence_url: "https://arxiv.org/licenses/nonexclusive-distrib/1.0/license.html"
summary_licence: "Elamur Cosmic License"
canonical: "https://research.elamur.ai/free/en/papers/kaliszyk-2018-reinforcement-learning-theorem-proving/"
---
[Elamur Research](https://md.research.elamur.ai/free/en/) · [this page in HTML](https://research.elamur.ai/free/en/papers/kaliszyk-2018-reinforcement-learning-theorem-proving/)

[home](https://md.research.elamur.ai/free/en/) / [papers](https://md.research.elamur.ai/free/en/papers/) / [2018](https://md.research.elamur.ai/free/en/papers/2018/page/5/) / Reinforcement Learning of Theorem Proving

# Reinforcement Learning of Theorem Proving

**Authors:** [Cezary Kaliszyk](https://md.research.elamur.ai/free/en/authors/cezary-kaliszyk/), [Josef Urban](https://md.research.elamur.ai/free/en/authors/josef-urban/), [Henryk Michalewski](https://md.research.elamur.ai/free/en/authors/henryk-michalewski/) and Mirek Olšák · **Year:** 2018 · **Venue:** arXiv:1805.07563 · **Licence:** [arXiv — non-exclusive licence to distribute](https://arxiv.org/licenses/nonexclusive-distrib/1.0/license.html)

**Links:** [Publisher's page](https://arxiv.org/abs/1805.07563) · [PDF](https://arxiv.org/pdf/1805.07563v1) · [DOI 10.48550/arxiv.1805.07563](https://doi.org/10.48550/arxiv.1805.07563) · [arXiv 1805.07563](https://arxiv.org/abs/1805.07563) · [OpenAlex](https://openalex.org/W2804556168)

**Citations:** 15 citations (OpenAlex, 2026-10-14) · [35](https://md.research.elamur.ai/free/en/papers/kaliszyk-2018-reinforcement-learning-theorem-proving/cited-by/) in our library, of the 149,439 papers whose bibliographies we read

## Summary
The paper asks whether a first-order theorem prover can learn its proof-search strategy from experience instead of relying on hand-crafted heuristics. The authors begin with mlCoP, an OCaml version of the connection-tableau prover leanCoP. They remove iterative deepening, which yields a deliberately incomplete "bare" prover that picks inferences at random. They then add three things: Monte-Carlo tree search driven by the UCT formula, a learned policy that estimates prior probabilities for inferences, and a learned value function that scores tableaux. The resulting system, rlCoP, repeatedly alternates between proving and learning on Mizar problems taken from the Miz40 dataset. Only training problems feed the learning, and evaluation uses held-out problems. Untrained, rlCoP is much weaker than standard mlCoP. After a few iterations, however, it solves over 40% more unseen problems under an equal inference budget. Typical published gains in the field are 3–10%, so this result suggests reinforcement learning can work for general mathematical reasoning at scale with almost no domain engineering.

## Key points
- **Training and evaluation:** rlCoP was trained on data from iterations 0–4 and then proved 1624 test problems in the 5th iteration. That is 42.1% more than mlCoP achieved with the same inference limit.
- **Overlap with the baseline:** after 10 iterations, rlCoP solved 577 test problems that mlCoP could not, while mlCoP solved 96 that rlCoP missed, for a net gain of 481. Some of rlCoP's proofs, such as WAYBEL_0:28, TOPREALC:10 and FUNCOP_1:34, were out of reach for mlCoP even at 4 million inferences.
- **Default value heuristic:** before the learned value function is introduced, a leaf is scored as 0.95 raised to the number of open goals. This rewards tableaux with fewer unclosed branches.
- **Tuned settings:** a small grid search set the UCT exploration constant c to 2 (with learned guidance) and the policy softmax temperature to 2.5. Training examples come only from bigstep nodes.
- **Comparison with AlphaZero-style selection:** using AlphaZero-style PUCT instead of UCT made practically no difference to the results.

*Our summary of the paper, in our own words — not its text. The work belongs to its authors; read it at the links above.*

## Institutions

- [Charles University](https://md.research.elamur.ai/free/en/universities/charles-university/) — University, Prague, Czechia · 135 works · 21,106 citations
- [Universität Innsbruck](https://md.research.elamur.ai/free/en/universities/universitat-innsbruck/) — University, Innsbruck, Austria · 23 works · 1,475 citations
- [Czech Technical University in Prague](https://md.research.elamur.ai/free/en/universities/czech-technical-university-in-prague/) — University, Prague, Czechia · 16 works · 930 citations
- [University of Warsaw](https://md.research.elamur.ai/free/en/universities/university-of-warsaw/) — University, Warsaw, Poland · 14 works · 774 citations

📚 Shelves (2): [🖥️ Computer Science](https://md.research.elamur.ai/free/en/shelves/computer-science/) · 19,503 works · [🤖 Artificial Intelligence](https://md.research.elamur.ai/free/en/shelves/computer-science/artificial-intelligence/) · 18,805 works

🧭 Topics (1): [🧮 Reasoning](https://md.research.elamur.ai/free/en/topics/reasoning/) · 1,948 works

## Cite

Cite as: Cezary Kaliszyk, Josef Urban, Henryk Michalewski and Mirek Olšák. 2018. Reinforcement Learning of Theorem Proving. arXiv:1805.07563.

The paper itself, not this page. BibTeX from the library's record of the work.

```bibtex
@misc{kaliszyk2018reinforcement,
  title = {{Reinforcement Learning of Theorem Proving}},
  author = {Cezary Kaliszyk, Josef Urban, Henryk Michalewski and Mirek Olšák},
  year = {2018},
  doi = {10.48550/arxiv.1805.07563},
  eprint = {1805.07563},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.1805.07563}
}
```

- [← previous Discourse Annotation in the PDTB: The Next Generation](https://md.research.elamur.ai/free/en/papers/prasad-2018-discourse-annotation-pdtb-next-generation/)
- [next → Universal Dependencies Version 2 for Japanese](https://md.research.elamur.ai/free/en/papers/asahara-2018-universal-dependencies-version-2-japanese/)
- [↑ back to papers of 2018](https://md.research.elamur.ai/free/en/papers/2018/page/5/)

## References

44 references, 10 of them with a card of ours. ↗ leads to the work, «find» searches for one we have no id for yet.

1. J. Alama, T. Heskes, D. Kühlwein, E. Tsivtsivadze, and J. Urban. [Premise selection for mathematics by corpus analysis and kernel methods](https://md.research.elamur.ai/free/en/papers/alama-2011-premise-selection-mathematics-corpus-analysis/). J. Autom. Reasoning, 52(2):191–213, 2014.
2. A. A. Alemi, F. Chollet, N. Eén, G. Irving, C. Szegedy, and J. Urban. [DeepMath - deep sequence models for premise selection](https://md.research.elamur.ai/free/en/papers/alemi-2016-deepmath-deep-sequence-models-premise/). In D. D. Lee, M. Sugiyama, U. V. Luxburg, I. Guyon, and R. Garnett, editors, Advances in Neural Information Processing Systems 29: Annual Conference on Neural Information Pro…
3. T. Anthony, Z. Tian, and D. Barber. [Thinking fast and slow with deep learning and tree search](https://md.research.elamur.ai/free/en/papers/anthony-2017-thinking-fast-slow-deep-learning/). In I. Guyon, U. von Luxburg, S. Bengio, H. M. Wallach, R. Fergus, S. V. N. Vishwanathan, and R. Garnett, editors, Advances in Neural Information Processing Systems 30: Annual Conference on Neural Informati…
4. L. Bachmair and H. Ganzinger. Rewrite-based equational theorem proving with selection and simplification. Journal of Logic and Computation, 4(3):217–247, 1994. [find](https://scholar.google.com/scholar?q=L%2E+Bachmair+and+H%2E+Ganzinger%2E+Rewrite%2Dbased+equational+theorem+proving+with+selection+and+simplification%2E+Journal+of+Logic+and+Computation%2C+4%283%29%3A217%E2%80%93247%2C+1994%2E)
5. C. W. Barrett, R. Sebastiani, S. A. Seshia, C. Tinelli, et al. Satisfiability modulo theories. Handbook of satisfiability, 185:825–885, 2009. [find](https://scholar.google.com/scholar?q=C%2E+W%2E+Barrett%2C+R%2E+Sebastiani%2C+S%2E+A%2E+Seshia%2C+C%2E+Tinelli%2C+et+al%2E+Satisfiability+modulo+theories%2E+Handbook+of+satisfiability%2C+185%3A825%E2%80%93885%2C+2009%2E)
6. J. C. Blanchette, D. Greenaway, C. Kaliszyk, D. Kühlwein, and J. Urban. A learning-based fact selector for Isabelle/HOL. J. Autom. Reasoning, 57(3):219–244, 2016. [find](https://scholar.google.com/scholar?q=J%2E+C%2E+Blanchette%2C+D%2E+Greenaway%2C+C%2E+Kaliszyk%2C+D%2E+Ku%CC%88hlwein%2C+and+J%2E+Urban%2E+A+learning%2Dbased+fact+selector+for+Isabelle%2FHOL%2E+J%2E+Autom%2E+Reasoning%2C+57%283%29%3A219%E2%80%93244%2C+2016%2E)
7. J. C. Blanchette, C. Kaliszyk, L. C. Paulson, and J. Urban. [Hammering towards QED](https://md.research.elamur.ai/free/en/papers/blanchette-2016-hammering-qed/). J. Formalized Reasoning, 9(1):101–148, 2016.
8. T. Chen and C. Guestrin. XGBoost: A scalable tree boosting system. In Proceedings of the 22Nd ACM SIGKDD International Conference on Knowledge Discovery and Data Mining, KDD ’16, pages 785–794, New York, NY, USA, 2016. ACM. [find](https://scholar.google.com/scholar?q=T%2E+Chen+and+C%2E+Guestrin%2E+XGBoost%3A+A+scalable+tree+boosting+system%2E+In+Proceedings+of+the+22Nd+ACM+SIGKDD+International+Conference+on+Knowledge+Discovery+and+Data+Mining%2C+KDD+%E2%80%9916%2C+pages+785%E2%80%93794%2C+New+Yo)
9. R.-E. Fan, K.-W. Chang, C.-J. Hsieh, X.-R. Wang, and C.-J. Lin. Liblinear: A library for large linear classification. Journal of machine learning research, 9(Aug):1871–1874, 2008. [find](https://scholar.google.com/scholar?q=R%2E%2DE%2E+Fan%2C+K%2E%2DW%2E+Chang%2C+C%2E%2DJ%2E+Hsieh%2C+X%2E%2DR%2E+Wang%2C+and+C%2E%2DJ%2E+Lin%2E+Liblinear%3A+A+library+for+large+linear+classification%2E+Journal+of+machine+learning+research%2C+9%28Aug%29%3A1871%E2%80%931874%2C+2008%2E)
10. M. Färber, C. Kaliszyk, and J. Urban. Monte Carlo tableau proof search. In L. de Moura, editor, 26th International Conference on Automated Deduction (CADE), volume 10395 of LNCS, pages 563–579. Springer, 2017. [find](https://scholar.google.com/scholar?q=M%2E+Fa%CC%88rber%2C+C%2E+Kaliszyk%2C+and+J%2E+Urban%2E+Monte+Carlo+tableau+proof+search%2E+In+L%2E+de+Moura%2C+editor%2C+26th+International+Conference+on+Automated+Deduction+%28CADE%29%2C+volume+10395+of+LNCS%2C+pages+563%E2%80%93579%2E+Sprin)
11. T. Gauthier and C. Kaliszyk. Premise selection and external provers for HOL4. In X. Leroy and A. Tiu, editors, Proc. of the 4th Conference on Certified Programs and Proofs (CPP’15), pages 49–57. ACM, 2015. [find](https://scholar.google.com/scholar?q=T%2E+Gauthier+and+C%2E+Kaliszyk%2E+Premise+selection+and+external+provers+for+HOL4%2E+In+X%2E+Leroy+and+A%2E+Tiu%2C+editors%2C+Proc%2E+of+the+4th+Conference+on+Certified+Programs+and+Proofs+%28CPP%E2%80%9915%29%2C+pages+49%E2%80%9357%2E+ACM%2C+)
12. T. Gauthier, C. Kaliszyk, and J. Urban. TacticToe: Learning to reason with HOL4 tactics. In T. Eiter and D. Sands, editors, 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, LPAR-21, volume 46 of EPiC Series in Computing, pages 125–143. EasyChair, 2017. [find](https://scholar.google.com/scholar?q=T%2E+Gauthier%2C+C%2E+Kaliszyk%2C+and+J%2E+Urban%2E+TacticToe%3A+Learning+to+reason+with+HOL4+tactics%2E+In+T%2E+Eiter+and+D%2E+Sands%2C+editors%2C+21st+International+Conference+on+Logic+for+Programming%2C+Artificial+Intellige)
13. A. Grabowski, A. Korniłowicz, and A. Naumowicz. Mizar in a nutshell. J. Formalized Reasoning, 3(2):153–245, 2010. [find](https://scholar.google.com/scholar?q=A%2E+Grabowski%2C+A%2E+Korni%C5%82owicz%2C+and+A%2E+Naumowicz%2E+Mizar+in+a+nutshell%2E+J%2E+Formalized+Reasoning%2C+3%282%29%3A153%E2%80%93245%2C+2010%2E)
14. T. Gransden, N. Walkinshaw, and R. Raman. SEPIA: search for proofs using inferred automata. In Automated Deduction - CADE-25 - 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings, pages 246–255, 2015. [find](https://scholar.google.com/scholar?q=T%2E+Gransden%2C+N%2E+Walkinshaw%2C+and+R%2E+Raman%2E+SEPIA%3A+search+for+proofs+using+inferred+automata%2E+In+Automated+Deduction+%2D+CADE%2D25+%2D+25th+International+Conference+on+Automated+Deduction%2C+Berlin%2C+Germany%2C+Au)
15. R. Hähnle. Tableaux and related methods. In Robinson and Voronkov [34], pages 100–178. [find](https://scholar.google.com/scholar?q=R%2E+Ha%CC%88hnle%2E+Tableaux+and+related+methods%2E+In+Robinson+and+Voronkov+%5B34%5D%2C+pages+100%E2%80%93178%2E)
16. J. Jakubuv and J. Urban. BliStrTune: hierarchical invention of theorem proving strategies. In Y. Bertot and V. Vafeiadis, editors, Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, pages 43–52. ACM, 2017. [find](https://scholar.google.com/scholar?q=J%2E+Jakubuv+and+J%2E+Urban%2E+BliStrTune%3A+hierarchical+invention+of+theorem+proving+strategies%2E+In+Y%2E+Bertot+and+V%2E+Vafeiadis%2C+editors%2C+Proceedings+of+the+6th+ACM+SIGPLAN+Conference+on+Certified+Programs+a)
17. J. Jakubuv and J. Urban. [ENIGMA: efficient learning-based inference guiding machine](https://md.research.elamur.ai/free/en/papers/jakubuv-2017-enigma-efficient-learning-based-inference/). In H. Geuvers, M. England, O. Hasan, F. Rabe, and O. Teschke, editors, Intelligent Computer Mathematics - 10th International Conference, CICM 2017, volume 10383 of Lecture Notes in Computer Science, pages 292–302. S…
18. C. Kaliszyk and J. Urban. [Learning-assisted automated reasoning with Flyspeck](https://md.research.elamur.ai/free/en/papers/kaliszyk-2012-learning-assisted-automated-reasoning-flyspeck/). J. Autom. Reasoning, 53(2):173–213, 2014.
19. C. Kaliszyk and J. Urban. FEMaLeCoP: Fairly efficient machine learning connection prover. In M. Davis, A. Fehnker, A. McIver, and A. Voronkov, editors, Logic for Programming, Artificial Intelligence, and Reasoning - 20th International Conference, volume 9450 of Lecture Notes in Computer Science, pag… [find](https://scholar.google.com/scholar?q=C%2E+Kaliszyk+and+J%2E+Urban%2E+FEMaLeCoP%3A+Fairly+efficient+machine+learning+connection+prover%2E+In+M%2E+Davis%2C+A%2E+Fehnker%2C+A%2E+McIver%2C+and+A%2E+Voronkov%2C+editors%2C+Logic+for+Programming%2C+Artificial+Intelligence%2C+)
20. C. Kaliszyk and J. Urban. [MizAR 40 for Mizar 40](https://md.research.elamur.ai/free/en/papers/kaliszyk-2013-mizar-40-mizar-40/). J. Autom. Reasoning, 55(3):245–256, 2015.
21. C. Kaliszyk, J. Urban, and J. Vyskočil. Machine learner for automated reasoning 0.4 and 0.5. In S. Schulz, L. de Moura, and B. Konev, editors, 4th Workshop on Practical Aspects of Automated Reasoning, PAAR@IJCAR 2014, Vienna, Austria, 2014, volume 31 of EPiC Series in Computing, pages 60–66. EasyCh… [find](https://scholar.google.com/scholar?q=C%2E+Kaliszyk%2C+J%2E+Urban%2C+and+J%2E+Vyskoc%CC%8Cil%2E+Machine+learner+for+automated+reasoning+0%2E4+and+0%2E5%2E+In+S%2E+Schulz%2C+L%2E+de+Moura%2C+and+B%2E+Konev%2C+editors%2C+4th+Workshop+on+Practical+Aspects+of+Automated+Reasoning)
22. C. Kaliszyk, J. Urban, and J. Vyskočil. Certified connection tableaux proofs for HOL Light and TPTP. In X. Leroy and A. Tiu, editors, Proc. of the 4th Conference on Certified Programs and Proofs (CPP’15), pages 59–66. ACM, 2015. [find](https://scholar.google.com/scholar?q=C%2E+Kaliszyk%2C+J%2E+Urban%2C+and+J%2E+Vyskoc%CC%8Cil%2E+Certified+connection+tableaux+proofs+for+HOL+Light+and+TPTP%2E+In+X%2E+Leroy+and+A%2E+Tiu%2C+editors%2C+Proc%2E+of+the+4th+Conference+on+Certified+Programs+and+Proofs+%28CPP)
23. L. Kocsis and C. Szepesvári. Bandit based monte-carlo planning. In J. Fürnkranz, T. Scheffer, and M. Spiliopoulou, editors, Machine Learning: ECML 2006, 17th European Conference on Machine Learning, volume 4212 of LNCS, pages 282–293. Springer, 2006. [find](https://scholar.google.com/scholar?q=L%2E+Kocsis+and+C%2E+Szepesva%CC%81ri%2E+Bandit+based+monte%2Dcarlo+planning%2E+In+J%2E+Fu%CC%88rnkranz%2C+T%2E+Scheffer%2C+and+M%2E+Spiliopoulou%2C+editors%2C+Machine+Learning%3A+ECML+2006%2C+17th+European+Conference+on+Machine+Learning%2C)
24. D. Kühlwein, T. van Laarhoven, E. Tsivtsivadze, J. Urban, and T. Heskes. Overview and evaluation of premise selection techniques for large theory mathematics. In B. Gramlich, D. Miller, and U. Sattler, editors, IJCAR, volume 7364 of LNCS, pages 378–392. Springer, 2012. [find](https://scholar.google.com/scholar?q=D%2E+Ku%CC%88hlwein%2C+T%2E+van+Laarhoven%2C+E%2E+Tsivtsivadze%2C+J%2E+Urban%2C+and+T%2E+Heskes%2E+Overview+and+evaluation+of+premise+selection+techniques+for+large+theory+mathematics%2E+In+B%2E+Gramlich%2C+D%2E+Miller%2C+and+U%2E+Sattle)
25. R. Letz, K. Mayr, and C. Goller. Controlled integration of the cut rule into connection tableau calculi. Journal of Automated Reasoning, 13:297–337, 1994. [find](https://scholar.google.com/scholar?q=R%2E+Letz%2C+K%2E+Mayr%2C+and+C%2E+Goller%2E+Controlled+integration+of+the+cut+rule+into+connection+tableau+calculi%2E+Journal+of+Automated+Reasoning%2C+13%3A297%E2%80%93337%2C+1994%2E)
26. S. M. Loos, G. Irving, C. Szegedy, and C. Kaliszyk. [Deep network guided proof search](https://md.research.elamur.ai/free/en/papers/loos-2017-deep-network-guided-proof-search/). In T. Eiter and D. Sands, editors, 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, LPAR-21, volume 46 of EPiC Series in Computing, pages 85–105. EasyChair, 2017.
27. W. McCune. Otter 2.0. In International Conference on Automated Deduction, pages 663–664. Springer, 1990. [find](https://scholar.google.com/scholar?q=W%2E+McCune%2E+Otter+2%2E0%2E+In+International+Conference+on+Automated+Deduction%2C+pages+663%E2%80%93664%2E+Springer%2C+1990%2E)
28. J. Meng and L. C. Paulson. Translating higher-order clauses to first-order clauses. J. Autom. Reasoning, 40(1):35–60, 2008. [find](https://scholar.google.com/scholar?q=J%2E+Meng+and+L%2E+C%2E+Paulson%2E+Translating+higher%2Dorder+clauses+to+first%2Dorder+clauses%2E+J%2E+Autom%2E+Reasoning%2C+40%281%29%3A35%E2%80%9360%2C+2008%2E)
29. J. Otten. Restricting backtracking in connection calculi. AI Commun., 23(2-3):159–182, 2010. [find](https://scholar.google.com/scholar?q=J%2E+Otten%2E+Restricting+backtracking+in+connection+calculi%2E+AI+Commun%2E%2C+23%282%2D3%29%3A159%E2%80%93182%2C+2010%2E)
30. J. Otten and W. Bibel. leanCoP: lean connection-based theorem proving. J. Symb. Comput., 36(1-2):139–161, 2003. [find](https://scholar.google.com/scholar?q=J%2E+Otten+and+W%2E+Bibel%2E+leanCoP%3A+lean+connection%2Dbased+theorem+proving%2E+J%2E+Symb%2E+Comput%2E%2C+36%281%2D2%29%3A139%E2%80%93161%2C+2003%2E)
31. F. Pedregosa, G. Varoquaux, A. Gramfort, V. Michel, B. Thirion, O. Grisel, M. Blondel, P. Prettenhofer, R. Weiss, V. Dubourg, J. Vanderplas, A. Passos, D. Cournapeau, M. Brucher, M. Perrot, and E. Duchesnay. Scikit-learn: Machine learning in Python. Journal of Machine Learning Research, 12:2825–2830… [find](https://scholar.google.com/scholar?q=F%2E+Pedregosa%2C+G%2E+Varoquaux%2C+A%2E+Gramfort%2C+V%2E+Michel%2C+B%2E+Thirion%2C+O%2E+Grisel%2C+M%2E+Blondel%2C+P%2E+Prettenhofer%2C+R%2E+Weiss%2C+V%2E+Dubourg%2C+J%2E+Vanderplas%2C+A%2E+Passos%2C+D%2E+Cournapeau%2C+M%2E+Brucher%2C+M%2E+Perrot%2C+and+E%2E+Duc)
32. B. Piotrowski and J. Urban. ATPboost: Learning premise selection in binary setting with ATP feedback. CoRR, abs/1802.03375, 2018. — [arXiv:1802.03375](https://arxiv.org/abs/1802.03375) [find](https://scholar.google.com/scholar?q=B%2E+Piotrowski+and+J%2E+Urban%2E+ATPboost%3A+Learning+premise+selection+in+binary+setting+with+ATP+feedback%2E+CoRR%2C+abs%2F1802%2E03375%2C+2018%2E+%E2%80%94+%5BarXiv%3A1802%2E03375%5D%28https%3A%2F%2Farxiv%2Eorg%2Fabs%2F1802%2E03375%29)
33. J. A. Robinson. A machine-oriented logic based on the resolution principle. Journal of the ACM (JACM), 12(1):23–41, 1965. [find](https://scholar.google.com/scholar?q=J%2E+A%2E+Robinson%2E+A+machine%2Doriented+logic+based+on+the+resolution+principle%2E+Journal+of+the+ACM+%28JACM%29%2C+12%281%29%3A23%E2%80%9341%2C+1965%2E)
34. J. A. Robinson and A. Voronkov, editors. Handbook of Automated Reasoning (in 2 volumes). Elsevier and MIT Press, 2001. [find](https://scholar.google.com/scholar?q=J%2E+A%2E+Robinson+and+A%2E+Voronkov%2C+editors%2E+Handbook+of+Automated+Reasoning+%28in+2+volumes%29%2E+Elsevier+and+MIT+Press%2C+2001%2E)
35. S. Schäfer and S. Schulz. Breeding theorem proving heuristics with genetic algorithms. In G. Gottlob, G. Sutcliffe, and A. Voronkov, editors, Global Conference on Artificial Intelligence, GCAI 2015, volume 36 of EPiC Series in Computing, pages 263–274. EasyChair, 2015. [find](https://scholar.google.com/scholar?q=S%2E+Scha%CC%88fer+and+S%2E+Schulz%2E+Breeding+theorem+proving+heuristics+with+genetic+algorithms%2E+In+G%2E+Gottlob%2C+G%2E+Sutcliffe%2C+and+A%2E+Voronkov%2C+editors%2C+Global+Conference+on+Artificial+Intelligence%2C+GCAI+2015%2C+)
36. D. Silver, A. Huang, C. J. Maddison, A. Guez, L. Sifre, G. van den Driessche, J. Schrittwieser, I. Antonoglou, V. Panneershelvam, M. Lanctot, S. Dieleman, D. Grewe, J. Nham, N. Kalchbrenner, I. Sutskever, T. P. Lillicrap, M. Leach, K. Kavukcuoglu, T. Graepel, and D. Hassabis. Mastering the game of G… [find](https://scholar.google.com/scholar?q=D%2E+Silver%2C+A%2E+Huang%2C+C%2E+J%2E+Maddison%2C+A%2E+Guez%2C+L%2E+Sifre%2C+G%2E+van+den+Driessche%2C+J%2E+Schrittwieser%2C+I%2E+Antonoglou%2C+V%2E+Panneershelvam%2C+M%2E+Lanctot%2C+S%2E+Dieleman%2C+D%2E+Grewe%2C+J%2E+Nham%2C+N%2E+Kalchbrenner%2C+I%2E+Sutske)
37. D. Silver, T. Hubert, J. Schrittwieser, I. Antonoglou, M. Lai, A. Guez, M. Lanctot, L. Sifre, D. Kumaran, T. Graepel, T. P. Lillicrap, K. Simonyan, and D. Hassabis. [Mastering chess and shogi by self-play with a general reinforcement learning algorithm](https://md.research.elamur.ai/free/en/papers/al-2017-mastering-chess-shogi-self-play/). CoRR, abs/1712.01815, 2017.
38. D. Silver, J. Schrittwieser, K. Simonyan, I. Antonoglou, A. Huang, A. Guez, T. Hubert, L. Baker, M. Lai, A. Bolton, et al. Mastering the game of go without human knowledge. Nature, 550(7676):354, 2017. [find](https://scholar.google.com/scholar?q=D%2E+Silver%2C+J%2E+Schrittwieser%2C+K%2E+Simonyan%2C+I%2E+Antonoglou%2C+A%2E+Huang%2C+A%2E+Guez%2C+T%2E+Hubert%2C+L%2E+Baker%2C+M%2E+Lai%2C+A%2E+Bolton%2C+et+al%2E+Mastering+the+game+of+go+without+human+knowledge%2E+Nature%2C+550%287676%29%3A354%2C+2017)
39. R. S. Sutton and A. G. Barto. Reinforcement learning: An introduction, volume 1. Cambridge Univ Press, 1998. [find](https://scholar.google.com/scholar?q=R%2E+S%2E+Sutton+and+A%2E+G%2E+Barto%2E+Reinforcement+learning%3A+An+introduction%2C+volume+1%2E+Cambridge+Univ+Press%2C+1998%2E)
40. J. Urban. MPTP 0.2: Design, implementation, and initial experiments. J. Autom. Reasoning, 37(1-2):21–43, 2006. [find](https://scholar.google.com/scholar?q=J%2E+Urban%2E+MPTP+0%2E2%3A+Design%2C+implementation%2C+and+initial+experiments%2E+J%2E+Autom%2E+Reasoning%2C+37%281%2D2%29%3A21%E2%80%9343%2C+2006%2E)
41. J. Urban. BliStr: The Blind Strategymaker. In G. Gottlob, G. Sutcliffe, and A. Voronkov, editors, Global Conference on Artificial Intelligence, GCAI 2015, volume 36 of EPiC Series in Computing, pages 312–319. EasyChair, 2015. [find](https://scholar.google.com/scholar?q=J%2E+Urban%2E+BliStr%3A+The+Blind+Strategymaker%2E+In+G%2E+Gottlob%2C+G%2E+Sutcliffe%2C+and+A%2E+Voronkov%2C+editors%2C+Global+Conference+on+Artificial+Intelligence%2C+GCAI+2015%2C+volume+36+of+EPiC+Series+in+Computing%2C+pages+)
42. J. Urban, G. Sutcliffe, P. Pudlák, and J. Vyskočil. MaLARea SG1 - Machine Learner for Automated Reasoning with Semantic Guidance. In A. Armando, P. Baumgartner, and G. Dowek, editors, IJCAR, volume 5195 of LNCS, pages 441–456. Springer, 2008. [find](https://scholar.google.com/scholar?q=J%2E+Urban%2C+G%2E+Sutcliffe%2C+P%2E+Pudla%CC%81k%2C+and+J%2E+Vyskoc%CC%8Cil%2E+MaLARea+SG1+%2D+Machine+Learner+for+Automated+Reasoning+with+Semantic+Guidance%2E+In+A%2E+Armando%2C+P%2E+Baumgartner%2C+and+G%2E+Dowek%2C+editors%2C+IJCAR%2C+volume+)
43. J. Urban, J. Vyskočil, and P. Štěpánek. MaLeCoP: Machine learning connection prover. In K. Brünnler and G. Metcalfe, editors, TABLEAUX, volume 6793 of LNCS, pages 263–277. Springer, 2011. [find](https://scholar.google.com/scholar?q=J%2E+Urban%2C+J%2E+Vyskoc%CC%8Cil%2C+and+P%2E+S%CC%8Cte%CC%8Cpa%CC%81nek%2E+MaLeCoP%3A+Machine+learning+connection+prover%2E+In+K%2E+Bru%CC%88nnler+and+G%2E+Metcalfe%2C+editors%2C+TABLEAUX%2C+volume+6793+of+LNCS%2C+pages+263%E2%80%93277%2E+Springer%2C+2011%2E)
44. D. Whalen. [Holophrasm: a neural automated theorem prover for higher-order logic](https://md.research.elamur.ai/free/en/papers/whalen-2016-holophrasm-neural-automated-theorem-prover/). CoRR, abs/1608.02644, 2016.

*Updated 3 November 2026*