Fetching the paper…
Reading the bibliography…
We present a reinforcement learning (RL) based guidance system for automated theorem proving geared towards Finding Longer Proofs (FLoP).
1903
Earlier work this paper cites.
1904
Earlier work this paper cites.
1905
Earlier work this paper cites.
1905
Earlier work this paper cites.
Robinson, R.M.: An essentially undecidable axiom system. Proceedings of the International Congress of Mathematics pp. 729–730 (1950)
1950
Earlier work this paper cites.
Polya, G.: Mathematics and Plausible Reasoning, Volume 1: Introduction and Analogy in Mathematics. Princeton University Press (1954)
1954
Earlier work this paper cites.
Polya, G.: How to Solve It. Princeton University Press (November 1971), http://www.amazon.com/exec/obidos/redirect?tag=citeulike07-20&path=ASIN/0691023565
1971
Earlier work this paper cites.
Peterson, J.G.: Shortest single axioms for the classical equivalential calculus. Notre Dame J. Formal Log. 17
1976
Earlier work this paper cites.
Kalman, J.A.: A shortest single axiom for the classical equivalential calculus. Notre Dame Journal of Formal Logic 19
1978
Earlier work this paper cites.
Bibel, W., Eder, E., Fronhöfer, B.: Towards an advanced implementation of the connection method. In: Bundy, A. (ed.) Proceedings of the 8th International Joint Conference on Artificial Intelligence. Karlsruhe, FRG, August 1983. pp. 920–922. William Kaufmann (1983), http://ijcai.org/Proceedings/83-2/Papers/072.pdf
1983
Earlier work this paper cites.
Wos, L., Winker, S., Smith, B., Veroff, R., Henschen, L.: A new use of an automated reasoning assistant: Open questions in equivalential calculus and the study of infinite domains. Artificial Intelligence 22
1984
Earlier work this paper cites.
Bledsoe, W.W.: Some thoughts on proof discovery. In: Proceedings of the 1986 Symposium on Logic Programming, Salt Lake City, Utah, USA, September 22-25, 1986. pp. 2–10. IEEE-CS (1986)
1986
Earlier work this paper cites.
Brock, B., Cooper, S., Pierce, W.: Analogical reasoning and proof discovery. In: Lusk, E., Overbeek, R. (eds.) 9th International Conference on Automated Deduction. pp. 454–468. Springer Berlin Heidelberg, Berlin, Heidelberg (1988)
1988
Earlier work this paper cites.
Bundy, A.: The use of explicit plans to guide inductive proofs. In: Lusk, E.L., Overbeek, R.A. (eds.) 9th International Conference on Automated Deduction, Argonne, Illinois, USA, May 23-26, 1988, Proceedings. Lecture Notes in Computer Science, vol. 310, pp. 111–120. Springer (1988). https://doi.org/10.1007/BFb0012826, https://doi.org/10.1007/BFb0012826
1988
Earlier work this paper cites.
Wos, L.: Meeting the challenge of fifty years of logic. J. Autom. Reason. 6
1990
Earlier work this paper cites.
McCune, W., Wos, L.: Experiments in automated deduction with condensed detachment. In: Kapur, D. (ed.) Automated Deduction - CADE-11, 11th International Conference on Automated Deduction, Saratoga Springs, NY, USA, June 15-18, 1992, Proceedings. Lecture Notes in Computer Science, vol. 607, pp. 209–223. Springer (1992). https://doi.org/10.1007/3-540-55602-8_167, https://doi.org/10.1007/3-540-55602-8_167
1992
Earlier work this paper cites.
Melis, E.: Theorem proving by analogy - A compelling example. In: Pinto-Ferreira, C.A., Mamede, N.J. (eds.) Progress in Artificial Intelligence, 7th Portuguese Conference on Artificial Intelligence, EPIA ’95, Funchal, Madeira Island, Portugal, October 3-6, 1995, Proceedings. Lecture Notes in Computer Science, vol. 990, pp. 261–272. Springer (1995). https://doi.org/10.1007/3-540-60428-6_22, https://doi.org/10.1007/3-540-60428-6_22
1995
Earlier work this paper cites.
Harrison, J.: HOL Light: A tutorial introduction. In: Srivas, M.K., Camilleri, A.J. (eds.) Formal Methods in Computer-Aided Design, First International Conference, FMCAD ’96, Palo Alto, California, USA, November 6-8, 1996, Proceedings. LNCS, vol. 1166, pp. 265–269. Springer (1996). https://doi.org/10.1007/BFb0031814, https://doi.org/10.1007/BFb0031814
1996
Earlier work this paper cites.
Veroff, R.: Using hints to increase the effectiveness of an automated reasoning program: Case studies. J. Autom. Reasoning 16
1996
Earlier work this paper cites.
Baader, F., Nipkow, T.: Term rewriting and all that. Cambridge University Press (1998)
1998
Cited alongside, same era.
Melis, E., Siekmann, J.H.: Knowledge-based proof planning. Artif. Intell. 115
1999
Cited alongside, same era.
Robinson, A., Voronkov, A. (eds.): Handbook of Automated Reasoning. Elsevier Science Publishers B. V., Amsterdam, The Netherlands, The Netherlands (2001)
2001
Cited alongside, same era.
Nipkow, T., Wenzel, M., Paulson, L.C.: Isabelle/HOL: A Proof Assistant for Higher-Order Logic. Springer-Verlag, Berlin, Heidelberg (2002)
2002
Cited alongside, same era.
Otten, J., Bibel, W.: leanCoP: lean connection-based theorem proving. J. Symb. Comput. 36
2003
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.
alphaXiv searches the wider corpus for related work and actual follow-ups.
alphaXiv is searching for related work…
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
Cited alongside, same era.
Urban, J.: MaLARea: a Metasystem for Automated Reasoning in Large Theories. In: Sutcliffe, G., Urban, J., Schulz, S. (eds.) Proceedings of the CADE-21 Workshop on Empirically Successful Automated Reasoning in Large Theories, Bremen, Germany, 17th July 2007. CEUR Workshop Proceedings, vol. 257. CEUR-WS.org (2007), http://ceur-ws.org/Vol-257/05_Urban.pdf
2007
Cited alongside, same era.
Urban, J., Sutcliffe, G., Pudlák, P., Vyskocil, J.: MaLARea SG1- machine learner for automated reasoning with semantic guidance. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) Automated Reasoning, 4th International Joint Conference, IJCAR 2008, Sydney, Australia, August 12-15, 2008, Proceedings. LNCS, vol. 5195, pp. 441–456. Springer (2008). https://doi.org/10.1007/978-3-540-71070-7_37, https://doi.org/10.1007/978-3-540-71070-7_37
2008
Cited alongside, same era.
2009
Cited alongside, same era.
Bertot, Y., Castran, P.: Interactive Theorem Proving and Program Development: Coq’Art The Calculus of Inductive Constructions. Springer Publishing Company, Incorporated, 1st edn. (2010)
2010
Cited alongside, same era.
Ross, S., Gordon, G., Bagnell, D.: A reduction of imitation learning and structured prediction to no-regret online learning. In: Gordon, G., Dunson, D., Dudik, 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.
Kinyon, M.K., Veroff, R., Vojtechovský, P.: Loops with abelian inner mapping groups: An application of automated deduction. In: Bonacina, M.P., Stickel, M.E. (eds.) Automated Reasoning and Mathematics - Essays in Memory of William W. McCune. LNCS, vol. 7788, pp. 151–164. Springer (2013). https://doi.org/10.1007/978-3-642-36675-8_8, https://doi.org/10.1007/978-3-642-36675-8_8
2013
Cited alongside, same era.
2017
Later among the works it cites.
Sutcliffe, G.: The TPTP Problem Library and Associated Infrastructure. From CNF to TH0, TPTP v6.4.0. Journal of Automated Reasoning 59
2017
Later among the works it cites.
Barrett, C.W., Tinelli, C.: Satisfiability modulo theories. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking, pp. 305–343. Springer (2018). https://doi.org/10.1007/978-3-319-10575-8_11, https://doi.org/10.1007/978-3-319-10575-8_11
2018
Later among the works it cites.
Hill, A., Raffin, A., Ernestus, M., Gleave, A., Kanervisto, A., Traore, R., Dhariwal, P., Hesse, C., Klimov, O., Nichol, A., Plappert, M., Radford, A., Schulman, J., Sidor, S., Wu, Y.: Stable baselines. https://github.com/hill-a/stable-baselines (2018)
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.
2018
Later among the works it cites.
2018
Later among the works it cites.
Sutton, R.S., Barto, A.G.: Reinforcement Learning: An Introduction. The MIT Press, second edn. (2018), http://incompleteideas.net/book/the-book-2nd.html
2018
Later among the works it cites.
Crouse, M., Abdelaziz, I., Makni, B., Whitehead, S., Cornelio, C., Kapanipathi, P., Srinivas, K., Thost, V., Witbrock, M., Fokoue, A.: A deep reinforcement learning approach to first-order logic theorem proving. arXiv: Artificial Intelligence (2019)
2019
Closest in time.
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
Closest in time.
Jakubův, J., Chvalovský, K., Olšák, M., Piotrowski, B., Suda, M., Urban, J.: Enigma anonymous: Symbol-independent inference guiding machine (system description). In: Peltier, N., Sofronie-Stokkermans, V. (eds.) Automated Reasoning. pp. 448–463. Springer International Publishing, Cham (2020)
2020
Closest in time.
Olsák, M., Kaliszyk, C., Urban, J.: Property invariant embedding for automated reasoning. In: Giacomo, G.D., Catalá, A., Dilkina, B., Milano, M., Barro, S., Bugarín, A., Lang, J. (eds.) ECAI 2020 - 24th European Conference on Artificial Intelligence, 29 August-8 September 2020, Santiago de Compostela, Spain, August 29 - September 8, 2020 - Including 10th Conference on Prestigious Applications of Artificial Intelligence (PAIS 2020). Frontiers in Artificial Intelligence and Applications, vol. 325, pp. 1395–1402. IOS Press (2020). https://doi.org/10.3233/FAIA200244, https://doi.org/10.3233/FAIA200244
2020
Closest in time.
Piotrowski, B., Urban, J.: Guiding inferences in connection tableau by recurrent neural networks. In: Benzmüller, C., Miller, B.R. (eds.) Intelligent Computer Mathematics - 13th International Conference, CICM 2020, Bertinoro, Italy, July 26-31, 2020, Proceedings. Lecture Notes in Computer Science, vol. 12236, pp. 309–314. Springer (2020). https://doi.org/10.1007/978-3-030-53518-6_23, https://doi.org/10.1007/978-3-030-53518-6_23
2020
Closest in time.
Rawson, M., Reger, G.: lazycop 0.1. EasyChair Preprint no. 3926 (EasyChair, 2020)
2020
Closest in time.
Urban, J., Jakubuv, J.: First neural conjecturing datasets and experiments. In: Benzmüller, C., Miller, B.R. (eds.) Intelligent Computer Mathematics - 13th International Conference, CICM 2020, Bertinoro, Italy, July 26-31, 2020, Proceedings. Lecture Notes in Computer Science, vol. 12236, pp. 315–323. Springer (2020). https://doi.org/10.1007/978-3-030-53518-6_24, https://doi.org/10.1007/978-3-030-53518-6_24
2020
Closest in time.
Zombori, Z., Urban, J., Brown, C.E.: Prolog technology reinforcement learning prover. In: Peltier, N., Sofronie-Stokkermans, V. (eds.) Automated Reasoning. pp. 489–507. Springer International Publishing, Cham (2020)
2020
Closest in time.