{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,5]],"date-time":"2025-07-05T13:10:06Z","timestamp":1751721006722,"version":"3.41.0"},"publisher-location":"Cham","reference-count":44,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319942049"},{"type":"electronic","value":"9783319942056"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","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":[[2018]]},"DOI":"10.1007\/978-3-319-94205-6_3","type":"book-chapter","created":{"date-parts":[[2018,6,29]],"date-time":"2018-06-29T16:22:50Z","timestamp":1530289370000},"page":"28-46","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":18,"title":["Superposition for Lambda-Free Higher-Order Logic"],"prefix":"10.1007","author":[{"given":"Alexander","family":"Bentkamp","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jasmin Christian","family":"Blanchette","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Simon","family":"Cruanes","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Uwe","family":"Waldmann","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,6,30]]},"reference":[{"key":"3_CR1","doi-asserted-by":"publisher","first-page":"965","DOI":"10.1016\/B978-044450813-3\/50017-5","volume-title":"Handbook of Automated Reasoning","author":"Peter B. Andrews","year":"2001","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)"},{"issue":"3","key":"3_CR2","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."},{"key":"3_CR3","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":"3_CR4","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"460","DOI":"10.1007\/978-3-540-25984-8_34","volume-title":"Automated Reasoning","author":"M Beeson","year":"2004","unstructured":"Beeson, M.: Lambda logic. In: Basin, D., Rusinowitch, M. (eds.) IJCAR 2004. LNCS (LNAI), vol. 3097, pp. 460\u2013474. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-25984-8_34"},{"key":"3_CR5","unstructured":"Bentkamp, A., Blanchette, J.C., Cruanes, S., Waldmann, U.: Superposition for lambda-free higher-order logic (technical report). Technical report (2018). http:\/\/matryoshka.gforge.inria.fr\/pubs\/lfhosup_report.pdf"},{"key":"3_CR6","first-page":"215","volume-title":"Computational Logic, Handbook of the History of Logic","author":"C Benzm\u00fcller","year":"2014","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, Amsterdam (2014)"},{"key":"3_CR7","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1007\/978-3-540-71070-7_14","volume-title":"Automated Reasoning","author":"C Benzm\u00fcller","year":"2008","unstructured":"Benzm\u00fcller, C., Paulson, L.C., Theiss, F., Fietzke, A.: LEO-II\u2014a cooperative automatic theorem prover for classical higher-order logic (system description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 162\u2013170. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-71070-7_14"},{"issue":"4:13","key":"3_CR8","first-page":"1","volume":"12","author":"JC Blanchette","year":"2016","unstructured":"Blanchette, J.C., B\u00f6hme, S., Popescu, A., Smallbone, N.: Encoding monomorphic and polymorphic types. Log. Methods Comput. Sci. 12(4:13), 1\u201352 (2016)","journal-title":"Log. Methods Comput. Sci."},{"issue":"1","key":"3_CR9","first-page":"101","volume":"9","author":"JC Blanchette","year":"2016","unstructured":"Blanchette, J.C., Kaliszyk, C., Paulson, L.C., Urban, J.: Hammering towards QED. J. Formaliz. Reason. 9(1), 101\u2013148 (2016)","journal-title":"J. Formaliz. Reason."},{"key":"3_CR10","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":"3_CR11","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":"3_CR12","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1007\/978-3-642-24364-6_7","volume-title":"Frontiers of Combining Systems","author":"F Bobot","year":"2011","unstructured":"Bobot, F., Paskevich, A.: Expressing polymorphic types in a many-sorted language. In: Tinelli, C., Sofronie-Stokkermans, V. (eds.) FroCoS 2011. LNCS (LNAI), vol. 6989, pp. 87\u2013102. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-24364-6_7"},{"issue":"1","key":"3_CR13","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1007\/s10817-011-9244-z","volume":"50","author":"M Bofill","year":"2013","unstructured":"Bofill, M., Rubio, A.: Paramodulation with non-monotonic orderings and simplification. J. Autom. Reason. 50(1), 51\u201398 (2013)","journal-title":"J. Autom. Reason."},{"key":"3_CR14","doi-asserted-by":"publisher","first-page":"412","DOI":"10.1137\/0204036","volume":"4","author":"D Brand","year":"1975","unstructured":"Brand, D.: Proving theorems with the modification method. SIAM J. Comput. 4, 412\u2013430 (1975)","journal-title":"SIAM J. Comput."},{"key":"3_CR15","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"},{"key":"3_CR16","unstructured":"Cruanes, S.: Extending superposition with integer arithmetic, structural induction, and beyond. Ph.D. thesis, \u00c9cole polytechnique (2015)"},{"key":"3_CR17","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":"3_CR18","doi-asserted-by":"crossref","unstructured":"Czajka, \u0141.: Improving automation in interactive theorem provers by efficient encoding of lambda-abstractions. In: Avigad, J., Chlipala, A. (eds.) CPP 2016, pp. 49\u201357. ACM (2016)","DOI":"10.1145\/2854065.2854069"},{"key":"3_CR19","doi-asserted-by":"crossref","unstructured":"Dowek, G., Hardin, T., Kirchner, C.: Higher-order unification via explicit substitutions (extended abstract). In: LICS 1995, pp. 366\u2013374. IEEE (1995)","DOI":"10.1109\/LICS.1995.523271"},{"key":"3_CR20","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-010-0411-4","volume-title":"Types, Tableaus, and G\u00f6del\u2019s God","author":"M Fitting","year":"2002","unstructured":"Fitting, M.: Types, Tableaus, and G\u00f6del\u2019s God. Kluwer, Dordrecht (2002)"},{"key":"3_CR21","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":"3_CR22","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":"3_CR23","first-page":"139","volume-title":"IJCAI 1973","author":"GP Huet","year":"1973","unstructured":"Huet, G.P.: A mechanization of type theory. In: Nilsson, N.J. (ed.) IJCAI 1973, pp. 139\u2013146. William Kaufmann, Burlington (1973)"},{"key":"3_CR24","first-page":"137","volume-title":"IJCAI 1991","author":"M Kerber","year":"1991","unstructured":"Kerber, M.: How to prove higher order theorems in first order logic. In: Mylopoulos, J., Reiter, R. (eds.) IJCAI 1991, pp. 137\u2013142. Morgan Kaufmann, Burlington (1991)"},{"key":"3_CR25","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":"3_CR26","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":"3_CR27","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":"3_CR28","doi-asserted-by":"publisher","first-page":"347","DOI":"10.1007\/BF00370646","volume":"46","author":"DA Miller","year":"1987","unstructured":"Miller, D.A.: A compact representation of proofs. Stud. Log. 46(4), 347\u2013370 (1987)","journal-title":"Stud. Log."},{"key":"3_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL: A Proof Assistant for Higher-Order Logic","author":"T Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL: A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45949-9"},{"key":"3_CR30","unstructured":"Peltier, N.: A variant of the superposition calculus. Archive of Formal Proofs (2016). https:\/\/www.isa-afp.org\/entries\/SuperCalc.shtml"},{"key":"3_CR31","first-page":"151","volume-title":"Machine Intelligence","author":"J Robinson","year":"1969","unstructured":"Robinson, J.: Mechanizing higher order logic. In: Meltzer, B., Michie, D. (eds.) Machine Intelligence, vol. 4, pp. 151\u2013170. Edinburgh University Press, Edinburgh (1969)"},{"key":"3_CR32","first-page":"121","volume-title":"Machine Intelligence","author":"J Robinson","year":"1970","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, Edinburgh (1970)"},{"key":"3_CR33","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":"3_CR34","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"310","DOI":"10.1007\/978-3-319-63046-5_19","volume-title":"Automated Deduction \u2013 CADE 26","author":"S Schulz","year":"2017","unstructured":"Schulz, S., Sutcliffe, G., Urban, J., Pease, A.: Detecting inconsistencies in large first-order knowledge bases. In: de Moura, L. (ed.) CADE 2017. LNCS (LNAI), vol. 10395, pp. 310\u2013325. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63046-5_19"},{"key":"3_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"150","DOI":"10.1007\/3-540-53904-2_93","volume-title":"Rewriting Techniques and Applications","author":"W Snyder","year":"1991","unstructured":"Snyder, W., Lynch, C.: Goal directed strategies for paramodulation. In: Book, R.V. (ed.) RTA 1991. LNCS, vol. 488, pp. 150\u2013161. Springer, Heidelberg (1991). https:\/\/doi.org\/10.1007\/3-540-53904-2_93"},{"key":"3_CR36","series-title":"Lecture Notes in Artificial Intelligence","first-page":"108","volume-title":"IJCAR 2018","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. LNAI, vol. 10900, pp. 108\u2013116. Springer, Cham (2018)"},{"key":"3_CR37","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"367","DOI":"10.1007\/978-3-319-08587-6_28","volume-title":"Automated Reasoning","author":"A Stump","year":"2014","unstructured":"Stump, A., Sutcliffe, G., Tinelli, C.: StarExec: a cross-community infrastructure for logic solving. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014. LNCS (LNAI), vol. 8562, pp. 367\u2013373. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08587-6_28"},{"issue":"6","key":"3_CR38","doi-asserted-by":"publisher","first-page":"419","DOI":"10.3233\/AIC-170744","volume":"30","author":"G Sutcliffe","year":"2017","unstructured":"Sutcliffe, G.: The CADE-26 automated theorem proving system competition\u2013CASC-26. AI Commun. 30(6), 419\u2013432 (2017)","journal-title":"AI Commun."},{"key":"3_CR39","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"},{"key":"3_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"406","DOI":"10.1007\/978-3-642-28717-6_32","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"G Sutcliffe","year":"2012","unstructured":"Sutcliffe, G., Schulz, S., Claessen, K., Baumgartner, P.: The TPTP typed first-order form with arithmetic. In: Bj\u00f8rner, N., Voronkov, A. (eds.) LPAR 2012. LNCS, vol. 7180, pp. 406\u2013419. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-28717-6_32"},{"key":"3_CR41","unstructured":"Vukmirovi\u0107, P.: Implementation of lambda-free higher-order superposition. M.Sc. thesis, Vrije Universiteit Amsterdam (2018)"},{"key":"3_CR42","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":"3_CR43","unstructured":"Wand, D.: Superposition: types and polymorphism. Ph.D. thesis, Universit\u00e4t des Saarlandes (2017)"},{"key":"3_CR44","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 Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-94205-6_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,5]],"date-time":"2025-07-05T12:50:55Z","timestamp":1751719855000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-94205-6_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319942049","9783319942056"],"references-count":44,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-94205-6_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]}}}