{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,18]],"date-time":"2025-05-18T18:21:11Z","timestamp":1747592471535,"version":"3.40.3"},"publisher-location":"Cham","reference-count":64,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030294359"},{"type":"electronic","value":"9783030294366"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019]]},"DOI":"10.1007\/978-3-030-29436-6_4","type":"book-chapter","created":{"date-parts":[[2019,8,20]],"date-time":"2019-08-20T16:04:02Z","timestamp":1566317042000},"page":"55-73","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":16,"title":["Superposition with Lambdas"],"prefix":"10.1007","author":[{"given":"Alexander","family":"Bentkamp","sequence":"first","affiliation":[]},{"given":"Jasmin","family":"Blanchette","sequence":"additional","affiliation":[]},{"given":"Sophie","family":"Tourret","sequence":"additional","affiliation":[]},{"given":"Petar","family":"Vukmirovi\u0107","sequence":"additional","affiliation":[]},{"given":"Uwe","family":"Waldmann","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2019,8,20]]},"reference":[{"issue":"3","key":"4_CR1","doi-asserted-by":"publisher","first-page":"414","DOI":"10.2307\/2269949","volume":"36","author":"PB Andrews","year":"1971","unstructured":"Andrews, P.B.: Resolution in type theory. J. Symb. Log. 36(3), 414\u2013432 (1971)","journal-title":"J. Symb. Log."},{"issue":"3","key":"4_CR2","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1007\/BF00248320","volume":"5","author":"PB Andrews","year":"1989","unstructured":"Andrews, P.B.: On connections and higher-order logic. J. Autom. Reason. 5(3), 257\u2013291 (1989)","journal-title":"J. Autom. Reason."},{"key":"4_CR3","doi-asserted-by":"crossref","unstructured":"Andrews, P.B.: Classical type theory. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. II, pp. 965\u20131007. Elsevier and MIT Press (2001)","DOI":"10.1016\/B978-044450813-3\/50017-5"},{"issue":"3","key":"4_CR4","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1007\/BF00252180","volume":"16","author":"PB Andrews","year":"1996","unstructured":"Andrews, P.B., Bishop, M., Issar, S., Nesmith, D., Pfenning, F., Xi, H.: TPS: a theorem-proving system for classical type theory. J. Autom. Reason. 16(3), 321\u2013353 (1996)","journal-title":"J. Autom. Reason."},{"issue":"3","key":"4_CR5","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1093\/logcom\/4.3.217","volume":"4","author":"L Bachmair","year":"1994","unstructured":"Bachmair, L., Ganzinger, H.: Rewrite-based equational theorem proving with selection and simplification. J. Log. Comput. 4(3), 217\u2013247 (1994)","journal-title":"J. Log. Comput."},{"issue":"4","key":"4_CR6","doi-asserted-by":"publisher","first-page":"451","DOI":"10.1007\/s10817-011-9233-2","volume":"47","author":"J Backes","year":"2011","unstructured":"Backes, J., Brown, C.E.: Analytic tableaux for higher-order logic with choice. J. Autom. Reason. 47(4), 451\u2013479 (2011)","journal-title":"J. Autom. Reason."},{"key":"4_CR7","unstructured":"Barbosa, H., Reynolds, A., Fontaine, P., El Ouraoui, D., Tinelli, C.: Higher-order SMT solving (work in progress). In: Dimitrova, R., D\u2019Silva, V. (eds.) SMT 2018 (2018)"},{"key":"4_CR8","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"432","DOI":"10.1007\/978-3-319-63046-5_27","volume-title":"Automated Deduction \u2013 CADE 26","author":"H Becker","year":"2017","unstructured":"Becker, H., Blanchette, J.C., Waldmann, U., Wand, D.: A transfinite Knuth\u2013Bendix order for lambda-free higher-order terms. In: de Moura, L. (ed.) CADE 2017. LNCS (LNAI), vol. 10395, pp. 432\u2013453. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63046-5_27"},{"key":"4_CR9","unstructured":"Bentkamp, A.: Formalization of the embedding path order for lambda-free higher-order terms. Archive of Formal Proofs (2018). http:\/\/isa-afp.org\/entries\/Lambda_Free_EPO.html"},{"key":"4_CR10","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"28","DOI":"10.1007\/978-3-319-94205-6_3","volume-title":"Automated Reasoning","author":"A Bentkamp","year":"2018","unstructured":"Bentkamp, A., Blanchette, J.C., Cruanes, S., Waldmann, U.: Superposition for lambda-free higher-order logic. In: Galmiche, D., Schulz, S., Sebastiani, R. (eds.) IJCAR 2018. LNCS (LNAI), vol. 10900, pp. 28\u201346. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-94205-6_3"},{"key":"4_CR11","doi-asserted-by":"crossref","unstructured":"Bentkamp, A., Blanchette, J., Tourret, S., Vukmirovi\u0107, P., Waldmann, U.: Superposition with lambdas (technical report). Technical report (2019). http:\/\/matryoshka.gforge.inria.fr\/pubs\/lamsup_report.pdf","DOI":"10.1007\/978-3-030-29436-6_4"},{"key":"4_CR12","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"399","DOI":"10.1007\/3-540-48660-7_39","volume-title":"Automated Deduction \u2014 CADE-16","author":"C Benzm\u00fcller","year":"1999","unstructured":"Benzm\u00fcller, C.: Extensional higher-order paramodulation and RUE-resolution. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol. 1632, pp. 399\u2013413. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48660-7_39"},{"key":"4_CR13","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"56","DOI":"10.1007\/BFb0054248","volume-title":"Automated Deduction \u2014 CADE-15","author":"C Benzm\u00fcller","year":"1998","unstructured":"Benzm\u00fcller, C., Kohlhase, M.: Extensional higher-order resolution. In: Kirchner, C., Kirchner, H. (eds.) CADE 1998. LNCS (LNAI), vol. 1421, pp. 56\u201371. Springer, Heidelberg (1998). https:\/\/doi.org\/10.1007\/BFb0054248"},{"key":"4_CR14","doi-asserted-by":"crossref","unstructured":"Benzm\u00fcller, C., Miller, D.: Automation of higher-order logic. In: Siekmann, J.H. (ed.) Computational Logic, Handbook of the History of Logic, vol. 9, pp. 215\u2013254. Elsevier (2014)","DOI":"10.1016\/B978-0-444-51624-4.50005-8"},{"issue":"6","key":"4_CR15","doi-asserted-by":"publisher","first-page":"881","DOI":"10.1093\/jigpal\/jzp080","volume":"18","author":"C Benzm\u00fcller","year":"2010","unstructured":"Benzm\u00fcller, C., Paulson, L.C.: Multimodal and intuitionistic logics in simple type theory. Log. J. IGPL 18(6), 881\u2013892 (2010)","journal-title":"Log. J. IGPL"},{"issue":"4","key":"4_CR16","doi-asserted-by":"publisher","first-page":"389","DOI":"10.1007\/s10817-015-9348-y","volume":"55","author":"C Benzm\u00fcller","year":"2015","unstructured":"Benzm\u00fcller, C., Sultana, N., Paulson, L.C., Theiss, F.: The higher-order prover Leo-II. J. Autom. Reason. 55(4), 389\u2013404 (2015)","journal-title":"J. Autom. Reason."},{"key":"4_CR17","unstructured":"Bhayat, A., Reger, G.: Set of support for higher-order reasoning. In: Konev, B., Urban, J., R\u00fcmmer, P. (eds.) PAAR-2018. CEUR Workshop Proceedings, vol. 2162, pp. 2\u201316. CEUR-WS.org (2018)"},{"key":"4_CR18","doi-asserted-by":"crossref","unstructured":"Blanchette, J.C., B\u00f6hme, S., Popescu, A., Smallbone, N.: Encoding monomorphic and polymorphic types. Log. Meth. Comput. Sci. 12(4) (2016)","DOI":"10.2168\/LMCS-12(4:13)2016"},{"key":"4_CR19","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"414","DOI":"10.1007\/978-3-642-38574-2_29","volume-title":"Automated Deduction \u2013 CADE-24","author":"JC Blanchette","year":"2013","unstructured":"Blanchette, J.C., Paskevich, A.: TFF1: the TPTP typed first-order form with rank-1 polymorphism. In: Bonacina, M.P. (ed.) CADE 2013. LNCS (LNAI), vol. 7898, pp. 414\u2013420. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-38574-2_29"},{"key":"4_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"461","DOI":"10.1007\/978-3-662-54458-7_27","volume-title":"Foundations of Software Science and Computation Structures","author":"JC Blanchette","year":"2017","unstructured":"Blanchette, J.C., Waldmann, U., Wand, D.: A lambda-free higher-order recursive path order. In: Esparza, J., Murawski, A.S. (eds.) FoSSaCS 2017. LNCS, vol. 10203, pp. 461\u2013479. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-662-54458-7_27"},{"key":"4_CR21","doi-asserted-by":"crossref","unstructured":"Blanqui, F., Jouannaud, J.P., Rubio, A.: The computability path ordering. Log. Meth. Comput. Sci. 11(4) (2015)","DOI":"10.2168\/LMCS-11(4:3)2015"},{"key":"4_CR22","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1007\/978-3-642-14203-1_9","volume-title":"Automated Reasoning","author":"S B\u00f6hme","year":"2010","unstructured":"B\u00f6hme, S., Nipkow, T.: Sledgehammer: Judgement Day. In: Giesl, J., H\u00e4hnle, R. (eds.) IJCAR 2010. LNCS (LNAI), vol. 6173, pp. 107\u2013121. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14203-1_9"},{"key":"4_CR23","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1007\/978-3-642-31365-3_11","volume-title":"Automated Reasoning","author":"CE Brown","year":"2012","unstructured":"Brown, C.E.: Satallax: an automatic higher-order prover. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS (LNAI), vol. 7364, pp. 111\u2013117. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31365-3_11"},{"issue":"5","key":"4_CR24","doi-asserted-by":"publisher","first-page":"381","DOI":"10.1016\/1385-7258(72)90034-0","volume":"75","author":"NG de Bruijn","year":"1972","unstructured":"de Bruijn, N.G.: Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem. Indag. Math. 75(5), 381\u2013392 (1972)","journal-title":"Indag. Math."},{"issue":"5","key":"4_CR25","doi-asserted-by":"publisher","first-page":"639","DOI":"10.1093\/logcom\/13.5.639","volume":"13","author":"I Cervesato","year":"2003","unstructured":"Cervesato, I., Pfenning, F.: A linear spine calculus. J. Log. Comput. 13(5), 639\u2013688 (2003)","journal-title":"J. Log. Comput."},{"key":"4_CR26","unstructured":"Cruanes, S.: Extending superposition with integer arithmetic, structural induction, and beyond. Ph.D. thesis, \u00c9cole polytechnique (2015)"},{"key":"4_CR27","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"172","DOI":"10.1007\/978-3-319-66167-4_10","volume-title":"Frontiers of Combining Systems","author":"S Cruanes","year":"2017","unstructured":"Cruanes, S.: Superposition with structural induction. In: Dixon, C., Finger, M. (eds.) FroCoS 2017. LNCS (LNAI), vol. 10483, pp. 172\u2013188. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66167-4_10"},{"key":"4_CR28","doi-asserted-by":"crossref","unstructured":"Czajka, \u0141., Kaliszyk, C.: Hammer for Coq: automation for dependent type theory (2018)","DOI":"10.1007\/s10817-018-9458-4"},{"issue":"2","key":"4_CR29","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1016\/0304-3975(93)90075-5","volume":"114","author":"DJ Dougherty","year":"1993","unstructured":"Dougherty, D.J.: Higher-order unification via combinators. Theor. Comput. Sci. 114(2), 273\u2013298 (1993)","journal-title":"Theor. Comput. Sci."},{"key":"4_CR30","doi-asserted-by":"crossref","unstructured":"Dowek, G.: Higher-order unification and matching. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. II, pp. 1009\u20131062. Elsevier and MIT Press (2001)","DOI":"10.1016\/B978-044450813-3\/50018-7"},{"key":"4_CR31","doi-asserted-by":"crossref","unstructured":"Fitting, M.: Types, Tableaus, and G\u00f6del\u2019s God. Kluwer (2002)","DOI":"10.1007\/978-94-010-0411-4"},{"issue":"1\u20132","key":"4_CR32","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/j.ic.2004.10.010","volume":"199","author":"H Ganzinger","year":"2005","unstructured":"Ganzinger, H., Stuber, J.: Superposition with equivalence reasoning and delayed clause normal form transformation. Inf. Comput. 199(1\u20132), 3\u201323 (2005)","journal-title":"Inf. Comput."},{"key":"4_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1007\/978-3-319-11936-6_14","volume-title":"Automated Technology for Verification and Analysis","author":"A Gupta","year":"2014","unstructured":"Gupta, A., Kov\u00e1cs, L., Kragl, B., Voronkov, A.: Extensional crisis and proving identity. In: Cassez, F., Raskin, J.-F. (eds.) ATVA 2014. LNCS, vol. 8837, pp. 185\u2013200. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-11936-6_14"},{"issue":"2","key":"4_CR34","doi-asserted-by":"publisher","first-page":"81","DOI":"10.2307\/2266967","volume":"15","author":"L Henkin","year":"1950","unstructured":"Henkin, L.: Completeness in the theory of types. J. Symb. Log. 15(2), 81\u201391 (1950)","journal-title":"J. Symb. Log."},{"key":"4_CR35","unstructured":"Huet, G.P.: A mechanization of type theory. In: Nilsson, N.J. (ed.) IJCAI 1973, pp. 139\u2013146. William Kaufmann (1973)"},{"issue":"1","key":"4_CR36","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1016\/0304-3975(75)90011-0","volume":"1","author":"GP Huet","year":"1975","unstructured":"Huet, G.P.: A unification algorithm for typed lambda-calculus. Theor. Comput. Sci. 1(1), 27\u201357 (1975)","journal-title":"Theor. Comput. Sci."},{"issue":"2","key":"4_CR37","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1016\/0304-3975(76)90021-9","volume":"3","author":"DC Jensen","year":"1976","unstructured":"Jensen, D.C., Pietrzykowski, T.: Mechanizing $$\\omega $$-order type theory through unification. Theor. Comput. Sci. 3(2), 123\u2013171 (1976)","journal-title":"Theor. Comput. Sci."},{"issue":"1\u20132","key":"4_CR38","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1016\/S0304-3975(98)00078-4","volume":"208","author":"JP Jouannaud","year":"1998","unstructured":"Jouannaud, J.P., Rubio, A.: Rewrite orderings for higher-order terms in eta-long beta-normal form and recursive path ordering. Theor. Comput. Sci. 208(1\u20132), 33\u201358 (1998)","journal-title":"Theor. Comput. Sci."},{"issue":"1","key":"4_CR39","doi-asserted-by":"publisher","first-page":"2:1","DOI":"10.1145\/1206035.1206037","volume":"54","author":"JP Jouannaud","year":"2007","unstructured":"Jouannaud, J.P., Rubio, A.: Polymorphic higher-order recursive path orderings. J. ACM 54(1), 2:1\u20132:48 (2007)","journal-title":"J. ACM"},{"key":"4_CR40","unstructured":"Kaliszyk, C., Sutcliffe, G., Rabe, F.: TH1: the TPTP typed higher-order form with rank-1 polymorphism. In: Fontaine, P., Schulz, S., Urban, J. (eds.) PAAR 2016. CEUR Workshop Proceedings, vol. 1635, pp. 41\u201355. CEUR-WS.org (2016)"},{"issue":"1","key":"4_CR41","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1007\/s11786-014-0182-0","volume":"9","author":"C Kaliszyk","year":"2015","unstructured":"Kaliszyk, C., Urban, J.: HOL(y)Hammer: online ATP service for HOL Light. Math. Comput. Sci. 9(1), 5\u201322 (2015)","journal-title":"Math. Comput. Sci."},{"key":"4_CR42","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"294","DOI":"10.1007\/3-540-59338-1_43","volume-title":"Theorem Proving with Analytic Tableaux and Related Methods","author":"M Kohlhase","year":"1995","unstructured":"Kohlhase, M.: Higher-order tableaux. In: Baumgartner, P., H\u00e4hnle, R., Possega, J. (eds.) TABLEAUX 1995. LNCS, vol. 918, pp. 294\u2013309. Springer, Heidelberg (1995). https:\/\/doi.org\/10.1007\/3-540-59338-1_43"},{"key":"4_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1007\/BFb0055140","volume-title":"Theorem Proving in Higher Order Logics","author":"K Konrad","year":"1998","unstructured":"Konrad, K.: Hot: a concurrent automated theorem prover based on higher-order tableaux. In: Grundy, J., Newey, M. (eds.) TPHOLs 1998. LNCS, vol. 1479, pp. 245\u2013261. Springer, Heidelberg (1998). https:\/\/doi.org\/10.1007\/BFb0055140"},{"key":"4_CR44","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-39799-8_1","volume-title":"Computer Aided Verification","author":"L Kov\u00e1cs","year":"2013","unstructured":"Kov\u00e1cs, L., Voronkov, A.: First-order theorem proving and Vampire. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 1\u201335. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_1"},{"key":"4_CR45","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"557","DOI":"10.1007\/978-3-319-21401-6_38","volume-title":"Automated Deduction - CADE-25","author":"T Libal","year":"2015","unstructured":"Libal, T.: Regular patterns in second-order unification. In: Felty, A.P., Middeldorp, A. (eds.) CADE 2015. LNCS (LNAI), vol. 9195, pp. 557\u2013571. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21401-6_38"},{"key":"4_CR46","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1007\/978-3-319-08587-6_5","volume-title":"Automated Reasoning","author":"F Lindblad","year":"2014","unstructured":"Lindblad, F.: A focused sequent calculus for higher-order logic. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014. LNCS (LNAI), vol. 8562, pp. 61\u201375. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08587-6_5"},{"issue":"1","key":"4_CR47","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/S0304-3975(97)00143-6","volume":"192","author":"R Mayr","year":"1998","unstructured":"Mayr, R., Nipkow, T.: Higher-order rewrite systems and their confluence. Theor. Comput. Sci. 192(1), 3\u201329 (1998)","journal-title":"Theor. Comput. Sci."},{"issue":"1","key":"4_CR48","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1007\/s10817-007-9085-y","volume":"40","author":"J Meng","year":"2008","unstructured":"Meng, J., Paulson, L.C.: Translating higher-order clauses to first-order clauses. J. Autom. Reason. 40(1), 35\u201360 (2008)","journal-title":"J. Autom. Reason."},{"issue":"4","key":"4_CR49","doi-asserted-by":"publisher","first-page":"497","DOI":"10.1093\/logcom\/1.4.497","volume":"1","author":"D Miller","year":"1991","unstructured":"Miller, D.: A logic programming language with lambda-abstraction, function variables, and simple unification. J. Log. Comput. 1(4), 497\u2013536 (1991)","journal-title":"J. Log. Comput."},{"key":"4_CR50","doi-asserted-by":"crossref","unstructured":"Nieuwenhuis, R., Rubio, A.: Paramodulation-based theorem proving. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. I, pp. 371\u2013443. Elsevier and MIT Press (2001)","DOI":"10.1016\/B978-044450813-3\/50009-6"},{"key":"4_CR51","unstructured":"Paulson, L.C., Blanchette, J.C.: Three years of experience with Sledgehammer, a practical link between automatic and interactive theorem provers. In: Sutcliffe, G., Schulz, S., Ternovska, E. (eds.) IWIL-2010. EPiC, vol. 2, pp. 1\u201311. EasyChair (2012)"},{"key":"4_CR52","unstructured":"Robinson, J.: Mechanizing higher order logic. In: Meltzer, B., Michie, D. (eds.) Machine Intelligence, vol. 4, pp. 151\u2013170. Edinburgh University Press (1969)"},{"key":"4_CR53","unstructured":"Robinson, J.: A note on mechanizing higher order logic. In: Meltzer, B., Michie, D. (eds.) Machine Intelligence, vol. 5, pp. 121\u2013135. Edinburgh University Press (1970)"},{"key":"4_CR54","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1007\/978-3-319-94205-6_7","volume-title":"Automated Reasoning","author":"A Schlichtkrull","year":"2018","unstructured":"Schlichtkrull, A., Blanchette, J.C., Traytel, D., Waldmann, U.: Formalizing Bachmair and Ganzinger\u2019s ordered resolution prover. In: Galmiche, D., Schulz, S., Sebastiani, R. (eds.) IJCAR 2018. LNCS (LNAI), vol. 10900, pp. 89\u2013107. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-94205-6_7"},{"key":"4_CR55","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"735","DOI":"10.1007\/978-3-642-45221-5_49","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"S Schulz","year":"2013","unstructured":"Schulz, S.: System description: E 1.8. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds.) LPAR 2013. LNCS, vol. 8312, pp. 735\u2013743. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-45221-5_49"},{"key":"4_CR56","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"573","DOI":"10.1007\/3-540-52885-7_115","volume-title":"10th International Conference on Automated Deduction","author":"W Snyder","year":"1990","unstructured":"Snyder, W.: Higher order E-unification. In: Stickel, M.E. (ed.) CADE 1990. LNCS (LNAI), vol. 449, pp. 573\u2013587. Springer, Heidelberg (1990). https:\/\/doi.org\/10.1007\/3-540-52885-7_115"},{"issue":"1\/2","key":"4_CR57","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1016\/S0747-7171(89)80023-9","volume":"8","author":"W Snyder","year":"1989","unstructured":"Snyder, W., Gallier, J.H.: Higher-order unification revisited: complete sets of transformations. J. Symb. Comput. 8(1\/2), 101\u2013140 (1989)","journal-title":"J. Symb. Comput."},{"key":"4_CR58","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1007\/978-3-319-94205-6_8","volume-title":"Automated Reasoning","author":"A Steen","year":"2018","unstructured":"Steen, A., Benzm\u00fcller, C.: The higher-order prover Leo-III. In: Galmiche, D., Schulz, S., Sebastiani, R. (eds.) IJCAR 2018. LNCS (LNAI), vol. 10900, pp. 108\u2013116. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-94205-6_8"},{"issue":"4","key":"4_CR59","doi-asserted-by":"publisher","first-page":"483","DOI":"10.1007\/s10817-017-9407-7","volume":"59","author":"G Sutcliffe","year":"2017","unstructured":"Sutcliffe, G.: The TPTP problem library and associated infrastructure-from CNF to TH0, TPTP v6.4.0. J. Autom. Reason. 59(4), 483\u2013502 (2017)","journal-title":"J. Autom. Reason."},{"key":"4_CR60","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"116","DOI":"10.1007\/978-3-642-02959-2_8","volume-title":"Automated Deduction \u2013 CADE-22","author":"G Sutcliffe","year":"2009","unstructured":"Sutcliffe, G., Benzm\u00fcller, C., Brown, C.E., Theiss, F.: Progress in the development of automated theorem proving for higher-order logic. In: Schmidt, R.A. (ed.) CADE 2009. LNCS (LNAI), vol. 5663, pp. 116\u2013130. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02959-2_8"},{"issue":"2","key":"4_CR61","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1007\/s10817-012-9269-y","volume":"50","author":"J Urban","year":"2013","unstructured":"Urban, J., Rudnicki, P., Sutcliffe, G.: ATP and presentation service for Mizar formalizations. J. Autom. Reason. 50(2), 229\u2013241 (2013)","journal-title":"J. Autom. Reason."},{"key":"4_CR62","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"192","DOI":"10.1007\/978-3-030-17462-0_11","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"P Vukmirovi\u0107","year":"2019","unstructured":"Vukmirovi\u0107, P., Blanchette, J.C., Cruanes, S., Schulz, S.: Extending a brainiac prover to lambda-free higher-order logic. In: Vojnar, T., Zhang, L. (eds.) TACAS 2019. LNCS, vol. 11427, pp. 192\u2013210. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-17462-0_11"},{"key":"4_CR63","unstructured":"Waldmann, U.: Automated reasoning II. Lecture notes, Max-Planck-Institut f\u00fcr Informatik (2016). http:\/\/resources.mpi-inf.mpg.de\/departments\/rg1\/teaching\/autrea2-ss16\/script-current.pdf"},{"key":"4_CR64","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"140","DOI":"10.1007\/978-3-642-02959-2_10","volume-title":"Automated Deduction \u2013 CADE-22","author":"C Weidenbach","year":"2009","unstructured":"Weidenbach, C., Dimova, D., Fietzke, A., Kumar, R., Suda, M., Wischnewski, P.: SPASS version 3.5. In: Schmidt, R.A. (ed.) CADE 2009. LNCS (LNAI), vol. 5663, pp. 140\u2013145. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02959-2_10"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE 27"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-29436-6_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,7,11]],"date-time":"2022-07-11T21:54:03Z","timestamp":1657576443000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-29436-6_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030294359","9783030294366"],"references-count":64,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-29436-6_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"20 August 2019","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":"Natal","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Brazil","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 August 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30 August 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cade2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.mat.ufrn.br\/CADE-27\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}