Fetching the paper…
Reading the bibliography…
We present a reinforcement learning toolkit for experiments with guiding automated theorem proving in the connection calculus.
1904
Earlier work this paper cites.
1911
Earlier work this paper cites.
Bibel, W.: Automated theorem proving. Artificial Intelligence, Vieweg, 2ed edn. (1987)
1987
Earlier work this paper cites.
Stickel, M.E.: A prolog technology theorem prover: Implementation by an extended prolog computer 4
1988
Earlier work this paper cites.
Andrews, P.B.: On Connections and Higher-Order Logic. Journal of Automated Reasoning 5
1989
Earlier work this paper cites.
Muggleton, S., Raedt, L.D.: Inductive logic programming: Theory and methods. J. Log. Program. 19/20
1994
Earlier work this paper cites.
Beckert, B., Posegga, J.: leantap: Lean tableau-based deduction. Journal of Automated Reasoning 15
1995
Earlier work this paper cites.
Sutton, R.S., Barto, A.G.: Reinforcement learning: An introduction, vol. 1. Cambridge Univ Press (1998)
1998
Earlier work this paper cites.
Letz, R., Stenz, G.: Model elimination and connection tableau procedures. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning (in 2 volumes), pp. 2015–2114. Elsevier and MIT Press (2001)
2001
Earlier work this paper cites.
Schulz, S.: E - A Brainiac Theorem Prover. AI Commun. 15
2002
Earlier work this paper cites.
Otten, J., Bibel, W.: leanCoP: lean connection-based theorem proving. J. Symb. Comput. 36
2003
Earlier work this paper cites.
Kocsis, L., Szepesvári, C.: Bandit based monte-carlo planning. In: Fürnkranz, J., Scheffer, T., Spiliopoulou, M. (eds.) Machine Learning: ECML 2006. pp. 282–293. Springer Berlin Heidelberg, Berlin, Heidelberg (2006)
2006
Earlier work this paper cites.
Urban, J.: MPTP 0.2: Design, implementation, and initial experiments. J. Autom. Reasoning 37
2006
Earlier work this paper cites.
Biere, A.: Picosat essentials. Journal on Satisfiability, Boolean Modeling and Computation (JSAT 4
2008
Cited alongside, same era.
Otten, J.: leanCoP 2.0 and ileanCoP 1.2: High performance lean theorem proving in classical and intuitionistic logic (system descriptions). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) Automated Reasoning, 4th International Joint Conference, IJCAR 2008, Sydney, Australia, August 12-15, 2008, Proceedings. Lecture Notes in Computer Science, vol. 5195, pp. 283–291. Springer (2008), https://doi.org/10.1007/978-3-540-71070-7_23
2008
Cited alongside, same era.
Urban, J., Sutcliffe, G., Pudlák, P., Vyskočil, J.: MaLARea SG1 - Machine Learner for Automated Reasoning with Semantic Guidance. In: IJCAR. pp. 441–456 (2008)
2008
Cited alongside, same era.
Lukácsy, G., Szeredi, P.: Efficient description logic reasoning in prolog: The dlog system. TPLP 9
2009
Cited alongside, same era.
Chen, T., Guestrin, C.: XGBoost: A scalable tree boosting system. In: Proceedings of the 22Nd ACM SIGKDD International Conference on Knowledge Discovery and Data Mining. pp. 785–794. KDD ’16 (2016), http://doi.acm.org/10.1145/2939672.2939785
2016
Later among the works it cites.
Silver, D., Huang, A., Maddison, C.J., Guez, A., Sifre, L., van den Driessche, G., Schrittwieser, J., Antonoglou, I., Panneershelvam, V., Lanctot, M., Dieleman, S., Grewe, D., Nham, J., Kalchbrenner, N., Sutskever, I., Lillicrap, T.P., Leach, M., Kavukcuoglu, K., Graepel, T., Hassabis, D.: Mastering the game of go with deep neural networks and tree search. Nature 529
2016
Later among the works it cites.
2017
Later among the works it cites.
alphaXiv searches the wider corpus for related work and actual follow-ups.
alphaXiv is searching for related work…
Ross, S., Gordon, G., Bagnell, D.: A reduction of imitation learning and structured prediction to no-regret online learning. In: Gordon, G., Dunson, D., Dudík, M. (eds.) Proceedings of the Fourteenth International Conference on Artificial Intelligence and Statistics. Proceedings of Machine Learning Research, vol. 15, pp. 627–635. PMLR, Fort Lauderdale, FL, USA (11–13 Apr 2011), http://proceedings.mlr.press/v15/ross11a.html
2011
Cited alongside, same era.
Urban, J., Vyskocil, J., Stepánek, P.: MaLeCoP: Machine learning connection prover. In: Brünnler, K., Metcalfe, G. (eds.) Automated Reasoning with Analytic Tableaux and Related Methods - 20th International Conference, TABLEAUX 2011, Bern, Switzerland, July 4-8, 2011. Proceedings. LNCS, vol. 6793, pp. 263–277. Springer (2011), https://doi.org/10.1007/978-3-642-22119-4_21
2011
Cited alongside, same era.
Browne, C., Powley, E.J., Whitehouse, D., Lucas, S.M., Cowling, P.I., Rohlfshagen, P., Tavener, S., Liebana, D.P., Samothrakis, S., Colton, S.: A survey of monte carlo tree search methods. IEEE Transactions on Computational Intelligence and AI in Games 4
2012
Cited alongside, same era.
Wielemaker, J., Schrijvers, T., Triska, M., Lager, T.: SWI-Prolog. Theory and Practice of Logic Programming 12
2012
Cited alongside, same era.
Kovács, L., Voronkov, A.: First-order theorem proving and Vampire. In: Sharygina, N., Veith, H. (eds.) CAV. LNCS, vol. 8044, pp. 1–35. Springer (2013)
2013
Cited alongside, same era.
Alama, J., Heskes, T., Kühlwein, D., Tsivtsivadze, E., Urban, J.: Premise selection for mathematics by corpus analysis and kernel methods. J. Autom. Reasoning 52
2014
Cited alongside, same era.
Otten, J.: MleanCoP: A connection prover for first-order modal logic. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) Automated Reasoning - 7th International Joint Conference, IJCAR 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 19-22, 2014. Proceedings. Lecture Notes in Computer Science, vol. 8562, pp. 269–276. Springer (2014). https://doi.org/10.1007/978-3-319-08587-6, https://doi.org/10.1007/978-3-319-08587-6_20
2014
Cited alongside, same era.
Kaliszyk, C., Urban, J.: FEMaLeCoP: Fairly efficient machine learning connection prover. In: Davis, M., Fehnker, A., McIver, A., Voronkov, A. (eds.) Logic for Programming, Artificial Intelligence, and Reasoning - 20th International Conference, 2015, Proceedings. Lecture Notes in Computer Science, vol. 9450, pp. 88–96. Springer (2015). https://doi.org/10.1007/978-3-662-48899-7, https://doi.org/10.1007/978-3-662-48899-7_7
2015
Cited alongside, same era.
Jakubuv, J., Urban, J.: ENIGMA: efficient learning-based inference guiding machine. In: Geuvers, H., England, M., Hasan, O., Rabe, F., Teschke, O. (eds.) Intelligent Computer Mathematics - 10th International Conference, CICM 2017, Edinburgh, UK, July 17-21, 2017, Proceedings. Lecture Notes in Computer Science, vol. 10383, pp. 292–302. Springer (2017). https://doi.org/10.1007/978-3-319-62075-6_20, https://doi.org/10.1007/978-3-319-62075-6_20
2017
Later among the works it cites.
Loos, S.M., Irving, G., Szegedy, C., Kaliszyk, C.: Deep network guided proof search. In: 21st International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR) (2017)
2017
Later among the works it cites.
2017
Later among the works it cites.
Silver, D., Schrittwieser, J., Simonyan, K., Antonoglou, I., Huang, A., Guez, A., Hubert, T., Baker, L., Lai, M., Bolton, A., et al.: Mastering the game of go without human knowledge. Nature 550
2017
Later among the works it cites.
2018
Later among the works it cites.
Kaliszyk, C., Urban, J., Michalewski, H., Olsák, M.: Reinforcement learning of theorem proving. In: NeurIPS. pp. 8836–8847 (2018)
2018
Later among the works it cites.
Chvalovský, K., Jakubuv, J., Suda, M., Urban, J.: ENIGMA-NG: efficient neural and gradient-boosted inference guidance for E. In: Fontaine, P. (ed.) Automated Deduction - CADE 27 - 27th International Conference on Automated Deduction, Natal, Brazil, August 27-30, 2019, Proceedings. Lecture Notes in Computer Science, vol. 11716, pp. 197–215. Springer (2019). https://doi.org/10.1007/978-3-030-29436-6, https://doi.org/10.1007/978-3-030-29436-6_12
2019
Later among the works it cites.
Goertzel, Z., Jakubuv, J., Urban, J.: ENIGMAWatch: ProofWatch meets ENIGMA. In: Cerrito, S., Popescu, A. (eds.) Automated Reasoning with Analytic Tableaux and Related Methods - 28th International Conference, TABLEAUX 2019, London, UK, September 3-5, 2019, Proceedings. Lecture Notes in Computer Science, vol. 11714, pp. 374–388. Springer (2019). https://doi.org/10.1007/978-3-030-29026-9, https://doi.org/10.1007/978-3-030-29026-9_21
2019
Later among the works it cites.
Jakubuv, J., Urban, J.: Hammering Mizar by learning clause guidance. In: Harrison, J., O’Leary, J., Tolmach, A. (eds.) 10th International Conference on Interactive Theorem Proving, ITP 2019, September 9-12, 2019, Portland, OR, USA. LIPIcs, vol. 141, pp. 34:1–34:8. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2019), https://doi.org/10.4230/LIPIcs.ITP.2019.34
2019
Later among the works it cites.
Zombori, Z., Urban, J.: Learning complex actions from proofs in theorem proving, accepted to AITP’20, http://aitp-conference.org/2020/abstract/paper_11.pdf
2020
Closest in time.