CoChat
Sign Up
Cited by 22Logic, programming, and type systemsAI-based Problem Solving and PlanningArtificial Intelligence Applications

The DOI matches its Crossref record; 4 of the 4 references it cites were found in a registry or an index.

Towards Finding Longer Proofs

Open access
Zombori, Zsolt, Csiszárik, Adrián, Michalewski, Henryk, Kaliszyk, Cezary, Urban, Josef·2021·Lecture Notes in Computer Science
DOI 10.1007/978-3-030-86059-2_10
Open this paper in CoChat — free accountOpen PDF

Overview

The claims and statistics of this paper haven’t been checked yet.

Run the check — free, no account needed. It reads the open-access text and checks the sources it cites.

A few free checks a day · papers already verified open instantly · results are public

Integrity signals

Registry

Crossref · 10.1007/978-3-030-86059-2_10

Cites

4 of 4 references verified0 citation errors · 0 not checkable

Statistics

Verification

Claims the paper makes

The claims and statistics of this paper haven’t been checked yet.

Run the check — free, no account needed. It reads the open-access text and checks the sources it cites.

A few free checks a day · papers already verified open instantly · results are public

Claims other papers make about this one

Each is checked against this paper’s own text: does it say what the citing paper says it does?

  • Synthetic data has long been recognized and used as an important ingredient in theorem proving.

    “Synthetic data has long been recognized and used as an important ingredient in theorem proving63–66.”

    From Solving olympiad geometry without human demonstrations (2024) · cites this paper as [64]

    The Introduction says the authors introduce a synthetic dataset for theorem proving, and the datasets discussion describes synthetic problems as a useful benchmark. These passages support the use and value of synthetic data in this paper, but do not establish that it has long been recognized as an important ingredient across theorem proving. (LLM, conf=0.83)

    Experimental — accuracy not yet measured

Self-check

Percentages, sums and reported differences re-computed from the paper’s own numbers.

The self-check needs the paper’s full text.

Citations

Cites

Flagged first, then by citations

Research works printed but not linked: 52

  1. Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998) · DOI
  2. Bansal, K., Loos, S.M., Rabe, M.N., Szegedy, C., Wilcox, S.: HOList: an environment for machine learning of higher-order theorem proving (extended version). CoRR abs/1904.03241 (2019). http://arxiv.org/abs/1904.03241 · arXiv
  3. Barrett, C., Tinelli, C.: Satisfiability modulo theories. In: Clarke, E., Henzinger, T., Veith, H., Bloem, R. (eds.) Handbook of Model Checking, pp. 305–343. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-10575-8_11 · DOI
  4. Bertot, Y., Castran, P.: Interactive Theorem Proving and Program Development: Coq’Art The Calculus of Inductive Constructions, 1st edn. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-662-07964-5 · DOI
  5. 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
  6. Bledsoe, W.W.: Some thoughts on proof discovery. In: Proceedings of the 1986 Symposium on Logic Programming, Salt Lake City, Utah, USA, 22–25 September 1986, pp. 2–10. IEEE-CS (1986)
  7. Brock, B., Cooper, S., Pierce, W.: Analogical reasoning and proof discovery. In: Lusk, E., Overbeek, R. (eds.) CADE 1988. LNCS, vol. 310, pp. 454–468. Springer, Heidelberg (1988). https://doi.org/10.1007/BFb0012849 · DOI
  8. Brockman, G., et al.: OpenAI gym. CoRR abs/1606.01540 (2016). http://arxiv.org/abs/1606.01540 · arXiv
  9. Bundy, A.: The use of explicit plans to guide inductive proofs. In: Lusk, E., Overbeek, R. (eds.) CADE 1988. LNCS, vol. 310, pp. 111–120. Springer, Heidelberg (1988). https://doi.org/10.1007/BFb0012826 · DOI
  10. Chvalovský, K., Jakubuv, J., Suda, M., Urban, J.: ENIGMA-NG: efficient neural and gradient-boosted inference guidance for E. CoRR abs/1903.03182 (2019). http://arxiv.org/abs/1903.03182 · arXiv
  11. Harrison, J.: HOL light: a tutorial introduction. In: Srivas, M., Camilleri, A. (eds.) FMCAD 1996. LNCS, vol. 1166, pp. 265–269. Springer, Heidelberg (1996). https://doi.org/10.1007/BFb0031814 · DOI
  12. 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.) IJCAR 2020. LNCS (LNAI), vol. 12167, pp. 448–463. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-51054-1_29 · DOI
  13. Jakubův, J., Urban, J.: ENIGMA: efficient learning-based inference guiding machine. In: Geuvers, H., England, M., Hasan, O., Rabe, F., Teschke, O. (eds.) CICM 2017. LNCS (LNAI), vol. 10383, pp. 292–302. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-62075-6_20 · DOI
  14. 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 · DOI
  15. Kaliszyk, C., Urban, J.: FEMaLeCoP: fairly efficient machine learning connection prover. In: Davis, M., Fehnker, A., McIver, A., Voronkov, A. (eds.) LPAR 2015. LNCS, vol. 9450, pp. 88–96. Springer, Heidelberg (2015). https://doi.org/10.1007/978-3-662-48899-7_7 · DOI
  16. Kaliszyk, C., Urban, J., Michalewski, H., Olsák, M.: Reinforcement learning of theorem proving. In: NeurIPS, pp. 8836–8847 (2018)
  17. Kaliszyk, C., Urban, J., Vyskočil, J.: Certified connection tableaux proofs for HOL Light and TPTP. In: Proceedings of the 2015 Conference on Certified Programs and Proofs, CPP ’15, pp. 59–66. ACM (2015). https://doi.org/10.1145/2676724.2693176. http://doi.acm.org/10.1145/2676724.2693176 · DOI
  18. Kaliszyk, C., Urban, J., Vyskočil, J.: Efficient semantic features for automated reasoning over large theories. In: Yang, Q., Wooldridge, M. (eds.) Proc. of the 24th International Joint Conference on Artificial Intelligence (IJCAI’15), pp. 3084–3090. AAAI Press (2015)
  19. Kalman, J.A.: A shortest single axiom for the classical equivalential calculus. Notre Dame J. Form. Logic 19(1), 141–144 (1978). https://doi.org/10.1305/ndjfl/1093888216 · DOI
  20. Kinyon, M., Veroff, R., Vojtěchovský, P.: Loops with abelian inner mapping groups: an application of automated deduction. In: Bonacina, M.P., Stickel, M.E. (eds.) Automated Reasoning and Mathematics. LNCS (LNAI), vol. 7788, pp. 151–164. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-36675-8_8 · DOI
  21. Kocsis, L., Szepesvári, C.: Bandit based Monte-Carlo planning. In: Fürnkranz, J., Scheffer, T., Spiliopoulou, M. (eds.) ECML 2006. LNCS (LNAI), vol. 4212, pp. 282–293. Springer, Heidelberg (2006). https://doi.org/10.1007/11871842_29 · DOI
  22. Kovács, L., Voronkov, A.: First-order theorem proving and Vampire. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 1–35. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39799-8_1 · DOI
  23. 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)
  24. McCune, W., Wos, L.: Experiments in automated deduction with condensed detachment. In: Kapur, D. (ed.) CADE 1992. LNCS, vol. 607, pp. 209–223. Springer, Heidelberg (1992). https://doi.org/10.1007/3-540-55602-8_167 · DOI
  25. Melis, E.: Theorem proving by analogy — A compelling example. In: Pinto-Ferreira, C., Mamede, N.J. (eds.) EPIA 1995. LNCS, vol. 990, pp. 261–272. Springer, Heidelberg (1995). https://doi.org/10.1007/3-540-60428-6_22 · DOI
  26. Melis, E., Siekmann, J.H.: Knowledge-based proof planning. Artif. Intell. 115(1), 65–105 (1999). https://doi.org/10.1016/S0004-3702(99)00076-4 · DOI
  27. Nipkow, T., Wenzel, M., Paulson, L.C.: Isabelle/HOL: A Proof Assistant for Higher-Order Logic. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45949-9 · DOI
  28. 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 · DOI
  29. Otten, J., Bibel, W.: leanCoP: lean connection-based theorem proving. J. Symb. Comput. 36, 139–161 (2003) · DOI
  30. Paliwal, A., Loos, S.M., Rabe, M.N., Bansal, K., Szegedy, C.: Graph representations for higher-order logic and theorem proving. CoRR abs/1905.10006 (2019). http://arxiv.org/abs/1905.10006 · arXiv
  31. Peterson, J.G.: Shortest single axioms for the classical equivalential calculus. Notre Dame J. Formal Log. 17(2), 267–271 (1976). https://doi.org/10.1305/ndjfl/1093887534 · DOI
  32. Piotrowski, B., Urban, J.: Guiding inferences in connection tableau by recurrent neural networks. In: Benzmüller, C., Miller, B. (eds.) CICM 2020. LNCS (LNAI), vol. 12236, pp. 309–314. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-53518-6_23 · DOI
  33. Polu, S., Sutskever, I.: Generative language modeling for automated theorem proving. CoRR abs/2009.03393 (2020). https://arxiv.org/abs/2009.03393 · arXiv
  34. Polya, G.: Mathematics and Plausible Reasoning. Introduction and Analogy in Mathematics, vol. 1. Princeton University Press, Princeton (1954) · DOI
  35. Polya, G.: How to Solve It. Princeton University Press (1971). http://www.amazon.com/exec/obidos/redirect?tag=citeulike07-20&path=ASIN/0691023565
  36. Rawson, M., Reger, G.: lazycop 0.1. EasyChair Preprint no. 3926 (2020, EasyChair)
  37. Resnick, C., Raileanu, R., Kapoor, S., Peysakhovich, A., Cho, K., Bruna, J.: Backplay: “Man muss immer umkehren". CoRR abs/1807.06919 (2018). http://arxiv.org/abs/1807.06919 · arXiv
  38. Robinson, A., Voronkov, A. (eds.): Handbook of Automated Reasoning. Elsevier Science Publishers B. V, Amsterdam (2001)
  39. Robinson, R.M.: An essentially undecidable axiom system. In: Proceedings of the International Congress of Mathematics, pp. 729–730 (1950)
  40. 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 (2011). http://proceedings.mlr.press/v15/ross11a.html
  41. Salimans, T., Chen, R.: Learning Montezuma’s Revenge from a single demonstration. CoRR abs/1812.03381 (2018). http://arxiv.org/abs/1812.03381 · arXiv
  42. Schulz, S.: System description: E 1.8. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds.) LPAR 2013. LNCS, vol. 8312, pp. 735–743. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-45221-5_49 · DOI
  43. Silver, D., et al.: Mastering the game of go without human knowledge. Nature 550, 354 (2017). https://doi.org/10.1038/nature24270 · DOI · Paper page
  44. Sutcliffe, G.: The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0. J. Autom. Reason. 59(4), 483–502 (2017) · DOI
  45. Sutton, R.S., Barto, A.G.: Reinforcement Learning: An Introduction, 2nd edn. The MIT Press (2018). http://incompleteideas.net/book/the-book-2nd.html
  46. 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
  47. Urban, J., Jakubův, J.: First neural conjecturing datasets and experiments. In: Benzmüller, C., Miller, B. (eds.) CICM 2020. LNCS (LNAI), vol. 12236, pp. 315–323. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-53518-6_24 · DOI
  48. Urban, J., Sutcliffe, G., Pudlák, P., Vyskočil, J.: MaLARea SG1 - machine learner for automated reasoning with semantic guidance. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 441–456. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-71070-7_37 · DOI
  49. Veroff, R.: Using hints to increase the effectiveness of an automated reasoning program: case studies. J. Autom. Reason. 16(3), 223–239 (1996) · DOI
  50. 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. Artifi. Intell. 22(3), 303–356 (1984) · DOI
  51. Wos, L.: Meeting the challenge of fifty years of logic. J. Autom. Reason. 6(2), 213–232 (1990) · DOI
  52. Zombori, Z., Urban, J., Brown, C.E.: Prolog technology reinforcement learning prover. In: Peltier, N., Sofronie-Stokkermans, V. (eds.) IJCAR 2020. LNCS (LNAI), vol. 12167, pp. 489–507. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-51054-1_33 · DOI

Cited by

Sorted by citations

Metadata

Authors
Zombori, Z., Csiszárik, A., Michalewski, H., Kaliszyk, C., & Urban, J.
Affiliations
  • Eötvös Loránd University (HU)
  • University of Warsaw (PL)
  • Universität Innsbruck (AT)
  • Czech Technical University in Prague (CZ)
Corresponding author
Zombori, Zsolt
ORCID
Venue
Lecture Notes in Computer Science
Publisher
Springer International Publishing
Published
2021
Pages
167-186
ISSN
  • 0302-9743 (ISSN-L)
  • 1611-3349
DOI
10.1007/978-3-030-86059-2_10
OpenAlex
W2947304943
Cited by
22
References
4
Citations by year
2026: 1 · 2025: 4 · 2024: 2 · 2023: 4 · 2022: 1 · 2021: 6
FWCI
2.30
Type
conference paper
Language
en
Open access
Licence
Locations
  • Lecture notes in computer science (publishedVersion)
  • Repository of the Academy's Library (Library of the Hungarian Academy of Sciences) (acceptedVersion)
  • arXiv (Cornell University) (submittedVersion)
  • arXiv (Cornell University)
Funders
  • European Commission
  • Akademia Górniczo-Hutnicza im. Stanislawa Staszica
  • Infrastruktura PL-Grid
  • Academic Computer Centre Cyfronet, AGH University of Science and Technology
  • European Social Fund
Topics
  • Physical Sciences › Computer Science › Software › Logic, programming, and type systems
  • Physical Sciences › Computer Science › Artificial Intelligence › AI-based Problem Solving and Planning
  • Physical Sciences › Computer Science › Artificial Intelligence › Artificial Intelligence Applications
Keywords
automated theorem proving, reinforcement learning

About these checks

Registry, retraction, Cites and statistics results are computed, not judged, with one exception: a printed reference that no index lists is read once by a model before it counts as a citation error. Claims are extracted by a model and kept only when their quote appears verbatim in the text; each cited source is then checked, with a model’s help, for whether it says what the claim relies on. Those verdicts can be wrong — read the claim’s quote and the cited source before relying on one.

Statistics and arithmetic are recomputed, not judged.

Confidence bands are shown only for fields calibrated on our annotated test set. None is calibrated yet, so no band is shown.

What counts as a claim ›How we measure confidence ›How we check this ›

Are you an author, or do you see a problem with this page? Request a review