{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,5]],"date-time":"2025-11-05T06:44:13Z","timestamp":1762325053024,"version":"3.40.3"},"publisher-location":"Cham","reference-count":41,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030798758"},{"type":"electronic","value":"9783030798765"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,7,5]],"date-time":"2021-07-05T00:00:00Z","timestamp":1625443200000},"content-version":"vor","delay-in-days":185,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>The state-of-the-art superposition-based theorem provers for first-order logic rely on simplification orderings on terms to constrain the applicability of inference rules, which in turn shapes the ensuing search space. The popular Knuth-Bendix simplification ordering is parameterized by <jats:italic>symbol precedence<\/jats:italic>\u2014a permutation of the predicate and function symbols of the input problem\u2019s signature. Thus, the choice of precedence has an indirect yet often substantial impact on the amount of work required to complete a proof search successfully.<\/jats:p><jats:p>This paper describes and evaluates a symbol precedence recommender, a machine learning system that estimates the best possible precedence based on observations of prover performance on a set of problems and random precedences. Using the graph convolutional neural network technology, the system does not presuppose the problems to be related or share a common signature. When coupled with the theorem prover Vampire and evaluated on the TPTP problem library, the recommender is found to outperform a state-of-the-art heuristic by more than 4\u00a0% on unseen problems.<\/jats:p>","DOI":"10.1007\/978-3-030-79876-5_30","type":"book-chapter","created":{"date-parts":[[2021,7,7]],"date-time":"2021-07-07T09:20:19Z","timestamp":1625649619000},"page":"525-542","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Neural Precedence Recommender"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-1822-2651","authenticated-orcid":false,"given":"Filip","family":"B\u00e1rtek","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0989-5800","authenticated-orcid":false,"given":"Martin","family":"Suda","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2021,7,5]]},"reference":[{"key":"30_CR1","doi-asserted-by":"publisher","unstructured":"Auer, P., Cesa-Bianchi, N., Fischer, P.: Finite-time analysis of the multiarmed bandit problem. Machine Learning 47(2-3), 235\u2013256 (2002). https:\/\/doi.org\/10.1023\/A:1013689704352","DOI":"10.1023\/A:1013689704352"},{"key":"30_CR2","unstructured":"Ba, J.L., Kiros, J.R., Hinton, G.E.: Layer normalization (Jul 2016), http:\/\/arxiv.org\/abs\/1607.06450"},{"key":"30_CR3","doi-asserted-by":"publisher","unstructured":"Bachmair, L., Derschowitz, N., Plaisted, D.A.: Completion without failure. In: A\u00eft-Kaci, H., Nivat, M. (eds.) Rewriting Techniques, pp. 1\u201330. Academic Press (1989). https:\/\/doi.org\/10.1016\/B978-0-12-046371-8.50007-9","DOI":"10.1016\/B978-0-12-046371-8.50007-9"},{"key":"30_CR4","doi-asserted-by":"publisher","unstructured":"Bachmair, L., Ganzinger, H.: Rewrite-based equational theorem proving with selection and simplification. J. Log. Comput. 4(3), 217\u2013247 (1994). https:\/\/doi.org\/10.1093\/logcom\/4.3.217","DOI":"10.1093\/logcom\/4.3.217"},{"key":"30_CR5","doi-asserted-by":"publisher","unstructured":"Bachmair, L., Ganzinger, H.: Resolution theorem proving. In: Robinson and Voronkov [31], pp. 19\u201399. https:\/\/doi.org\/10.1016\/b978-044450813-3\/50004-7","DOI":"10.1016\/b978-044450813-3\/50004-7"},{"key":"30_CR6","unstructured":"B\u00e1rtek, F., Suda, M.: Learning precedences from simple symbol features. In: Fontaine et al. [10], pp. 21\u201333, http:\/\/ceur-ws.org\/Vol-2752\/paper2.pdf"},{"key":"30_CR7","doi-asserted-by":"publisher","unstructured":"Burges, C., Shaked, T., Renshaw, E., Lazier, A., Deeds, M., Hamilton, N., Hullender, G.: Learning to rank using gradient descent. In: ICML 2005 - Proceedings of the 22nd International Conference on Machine Learning. pp. 89\u201396. ACM Press, New York, New York, USA (2005). https:\/\/doi.org\/10.1145\/1102351.1102363","DOI":"10.1145\/1102351.1102363"},{"key":"30_CR8","doi-asserted-by":"publisher","unstructured":"Chvalovsk\u00fd, K., Jakub\u016fv, J., Suda, M., Urban, J.: ENIGMA-NG: Efficient neural and gradient-boosted inference guidance for E. In: Fontaine [9]. https:\/\/doi.org\/10.1007\/978-3-030-29436-6_12","DOI":"10.1007\/978-3-030-29436-6_12"},{"key":"30_CR9","doi-asserted-by":"publisher","unstructured":"Fontaine, P. (ed.): Automated Deduction - CADE 27, LNCS, vol. 11716. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-29436-6","DOI":"10.1007\/978-3-030-29436-6"},{"key":"30_CR10","unstructured":"Fontaine, P., Korovin, K., Kotsireas, I.S., R\u00fcmmer, P., Tourret, S. (eds.): Joint Proceedings of the 7th Workshop on Practical Aspects of Automated Reasoning (PAAR) and the 5th Satisfiability Checking and Symbolic Computation Workshop (SC-Square) Workshop, 2020 co-located with the 10th International Joint Conference on Automated Reasoning (IJCAR 2020). No.\u00a02752 in CEUR Workshop Proceedings, CEUR-WS.org, Aachen (2020), http:\/\/ceur-ws.org\/Vol-2752"},{"key":"30_CR11","doi-asserted-by":"publisher","unstructured":"Ganzinger, H., de Nivelle, H.: A superposition decision procedure for the guarded fragment with equality. In: 14th Annual IEEE Symposium on Logic in Computer Science. pp. 295\u2013303. IEEE Computer Society (1999). https:\/\/doi.org\/10.1109\/LICS.1999.782624","DOI":"10.1109\/LICS.1999.782624"},{"key":"30_CR12","unstructured":"Goodfellow, I.J., Bengio, Y., Courville, A.C.: Deep Learning. Adaptive computation and machine learning, MIT Press (2016), http:\/\/www.deeplearningbook.org\/"},{"key":"30_CR13","doi-asserted-by":"publisher","unstructured":"Harrison, J.: Handbook of Practical Logic and Automated Reasoning. Cambridge University Press, Cambridge (2009). https:\/\/doi.org\/10.1017\/CBO9780511576430","DOI":"10.1017\/CBO9780511576430"},{"key":"30_CR14","doi-asserted-by":"publisher","unstructured":"Hustadt, U., Konev, B., Schmidt, R.A.: Deciding monodic fragments by temporal resolution. In: Nieuwenhuis, R. (ed.) Automated Deduction - CADE-20. LNCS, vol. 3632, pp. 204\u2013218. Springer, Berlin, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11532231_15","DOI":"10.1007\/11532231_15"},{"key":"30_CR15","doi-asserted-by":"publisher","unstructured":"Jakub\u016fv, J., Chvalovsk\u00fd, K., Ol\u0161\u00e1k, M., Piotrowski, B., Suda, M., Urban, J.: ENIGMA Anonymous: Symbol-independent inference guiding\u00c2 machine (system description). In: Peltier, N., Sofronie-Stokkermans, V. (eds.) Automated Reasoning. LNCS, vol. 12167, pp. 448\u2013463. Springer, Cham (Jul 2020). https:\/\/doi.org\/10.1007\/978-3-030-51054-1_29","DOI":"10.1007\/978-3-030-51054-1_29"},{"key":"30_CR16","unstructured":"Kamin, S.N., L\u00e9vy, J.: Two generalizations of the recursive path ordering (1980), http:\/\/www.cs.tau.ac.il\/~nachumd\/term\/kamin-levy80spo.pdf, unpublished letter to Nachum Dershowitz"},{"key":"30_CR17","unstructured":"Kingma, D.P., Ba, J.: Adam: A method for stochastic optimization (Dec 2014), http:\/\/arxiv.org\/abs\/1412.6980"},{"key":"30_CR18","unstructured":"Kipf, T.N., Welling, M.: Semi-supervised classification with graph convolutional networks. In: 5th International Conference on Learning Representations, ICLR 2017 (Sep 2017), https:\/\/openreview.net\/forum?id=SJU4ayYgl"},{"key":"30_CR19","doi-asserted-by":"publisher","unstructured":"Knuth, D.E., Bendix, P.B.: Simple word problems in universal algebras. In: Siekmann and Wrightson [35], pp. 342\u2013376. https:\/\/doi.org\/10.1007\/978-3-642-81955-1_23","DOI":"10.1007\/978-3-642-81955-1_23"},{"key":"30_CR20","doi-asserted-by":"publisher","unstructured":"Kov\u00e1cs, L., Moser, G., Voronkov, A.: On transfinite Knuth-Bendix orders. In: Bj\u00f8rner, N., Sofronie-Stokkermans, V. (eds.) Automated Deduction - CADE-23. LNCS, vol. 6803, pp. 384\u2013399. Springer, Berlin, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22438-6_29","DOI":"10.1007\/978-3-642-22438-6_29"},{"key":"30_CR21","doi-asserted-by":"publisher","unstructured":"Kov\u00e1cs, L., Voronkov, A.: First-order theorem proving and Vampire. In: Sharygina, N., Veith, H. (eds.) Computer Aided Verification. LNCS, vol. 8044, pp. 1\u201335. Springer, Berlin, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_1","DOI":"10.1007\/978-3-642-39799-8_1"},{"key":"30_CR22","doi-asserted-by":"publisher","unstructured":"Ludwig, M., Waldmann, U.: An extension of the Knuth-Bendix ordering with LPO-like properties. In: Dershowitz, N., Voronkov, A. (eds.) Logic for Programming, Artificial Intelligence, and Reasoning. LNCS, vol. 4790, pp. 348\u2013362. Springer, Berlin, Heidelberg (Oct 2007). https:\/\/doi.org\/10.1007\/978-3-540-75560-9_26","DOI":"10.1007\/978-3-540-75560-9_26"},{"key":"30_CR23","unstructured":"Mohri, M., Rostamizadeh, A., Talwalkar, A.: Foundations of Machine Learning. MIT Press, 2 edn. (2018), https:\/\/cs.nyu.edu\/~mohri\/mlbook\/"},{"key":"30_CR24","doi-asserted-by":"publisher","unstructured":"Nieuwenhuis, R., Rubio, A.: Paramodulation-based theorem proving. In: Robinson and Voronkov [31], pp. 371\u2013443. https:\/\/doi.org\/10.1016\/b978-044450813-3\/50009-6","DOI":"10.1016\/b978-044450813-3\/50009-6"},{"key":"30_CR25","doi-asserted-by":"publisher","unstructured":"Nonnengart, A., Weidenbach, C.: Computing small clause normal forms. In: Robinson and Voronkov [31], pp. 335\u2013367. https:\/\/doi.org\/10.1016\/b978-044450813-3\/50008-4","DOI":"10.1016\/b978-044450813-3\/50008-4"},{"key":"30_CR26","doi-asserted-by":"publisher","unstructured":"Ol\u0161\u00e1k, M., Kaliszyk, C., Urban, J.: Property invariant embedding for automated reasoning. In: Giacomo, G.D., Catal\u00e1, A., Dilkina, B., Milano, M., Barro, S., Bugar\u00edn, A., Lang, J. (eds.) ECAI 2020\u201324th European Conference on Artificial Intelligence. Frontiers in Artificial Intelligence and Applications, vol. 325, pp. 1395\u20131402. IOS Press (2020). https:\/\/doi.org\/10.3233\/FAIA200244","DOI":"10.3233\/FAIA200244"},{"key":"30_CR27","unstructured":"Rawson, M., Reger, G.: Directed graph networks for logical reasoning (extended abstract). In: Fontaine et al. [10], pp. 109\u2013119, http:\/\/ceur-ws.org\/Vol-2752\/paper8.pdf"},{"key":"30_CR28","unstructured":"Reger, G., Suda, M.: Measuring progress to predict success: Can a good proof strategy be evolved? In: AITP 2017. pp. 20\u201321 (2017), http:\/\/aitp-conference.org\/2017\/aitp17-proceedings.pdf"},{"key":"30_CR29","doi-asserted-by":"publisher","unstructured":"Reger, G., Suda, M., Voronkov, A.: New techniques in clausal form generation. In: Benzm\u00fcller, C., Sutcliffe, G., Rojas, R. (eds.) GCAI 2016. 2nd Global Conference on Artificial Intelligence. EPiC Series in Computing, vol. 41, pp. 11\u201323. EasyChair (2016). https:\/\/doi.org\/10.29007\/dzfz","DOI":"10.29007\/dzfz"},{"key":"30_CR30","doi-asserted-by":"publisher","unstructured":"Robinson, G., Wos, L.: Paramodulation and theorem-proving in first-order theories with equality. In: Siekmann and Wrightson [35], pp. 298\u2013313. https:\/\/doi.org\/10.1007\/978-3-642-81955-1_19","DOI":"10.1007\/978-3-642-81955-1_19"},{"key":"30_CR31","unstructured":"Robinson, J.A., Voronkov, A. (eds.): Handbook of Automated Reasoning (in 2 volumes). Elsevier and MIT Press (2001)"},{"key":"30_CR32","doi-asserted-by":"publisher","unstructured":"Schlichtkrull, M.S., Kipf, T.N., Bloem, P., van den Berg, R., Titov, I., Welling, M.: Modeling relational data with graph convolutional networks. In: Gangemi, A., Navigli, R., Vidal, M., Hitzler, P., Troncy, R., Hollink, L., Tordai, A., Alam, M. (eds.) The Semantic Web. LNCS, vol. 10843, pp. 593\u2013607. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-93417-4_38","DOI":"10.1007\/978-3-319-93417-4_38"},{"key":"30_CR33","unstructured":"Schulz, S.: E 2.4 user manual. EasyChair preprint no. 2272, Manchester (2020), https:\/\/easychair.org\/publications\/preprint\/8dss"},{"key":"30_CR34","doi-asserted-by":"publisher","unstructured":"Schulz, S., Cruanes, S., Vukmirovi\u0107, P.: Faster, higher, stronger: E 2.3. In: Fontaine [9], pp. 495\u2013507. https:\/\/doi.org\/10.1007\/978-3-030-29436-6_29","DOI":"10.1007\/978-3-030-29436-6_29"},{"key":"30_CR35","unstructured":"Siekmann, J.H., Wrightson, G. (eds.): Springer, Berlin, Heidelberg (1983)"},{"key":"30_CR36","doi-asserted-by":"publisher","unstructured":"Sutcliffe, Geoff: The TPTP Problem Library and Associated Infrastructure. Journal of Automated Reasoning 59(4), 483\u2013502 (2017). https:\/\/doi.org\/10.1007\/s10817-017-9407-7","DOI":"10.1007\/s10817-017-9407-7"},{"key":"30_CR37","unstructured":"Sutton, R.S., Barto, A.G.: Reinforcement Learning: An Introduction. The MIT Press, 2 edn. (2018), http:\/\/incompleteideas.net\/book\/the-book-2nd.html"},{"key":"30_CR38","unstructured":"TPTP syntax, http:\/\/www.tptp.org\/TPTP\/SyntaxBNF.html"},{"key":"30_CR39","doi-asserted-by":"publisher","unstructured":"Voronkov, A.: AVATAR: The architecture for first-order theorem provers. In: Biere, A., Bloem, R. (eds.) Computer Aided Verification. LNCS, vol. 8559, pp. 696\u2013710. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_46","DOI":"10.1007\/978-3-319-08867-9_46"},{"key":"30_CR40","doi-asserted-by":"publisher","unstructured":"Weidenbach, C., Dimova, D., Fietzke, A., Kumar, R., Suda, M., Wischnewski, P.: SPASS version 3.5. In: Schmidt, R.A. (ed.) Automated Deduction - CADE-22. LNCS, vol. 5663, pp. 140\u2013145. Springer, Berlin, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02959-2_10","DOI":"10.1007\/978-3-642-02959-2_10"},{"key":"30_CR41","unstructured":"Zhou, J., Cui, G., Zhang, Z., Yang, C., Liu, Z., Wang, L., Li, C., Sun, M.: Graph neural networks: A review of methods and applications (Dec 2018), http:\/\/arxiv.org\/abs\/1812.08434"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE 28"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-79876-5_30","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,7,7]],"date-time":"2021-07-07T09:35:15Z","timestamp":1625650515000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-79876-5_30"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030798758","9783030798765"],"references-count":41,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-79876-5_30","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"5 July 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CADE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Automated Deduction","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12 July 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15 July 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cade2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.cs.cmu.edu\/~mheule\/CADE28\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"76","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"29","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"38% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"5","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"2 invited papers and 7 system descriptions are also included.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}