{"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":1747592471915,"version":"3.40.3"},"publisher-location":"Cham","reference-count":32,"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_5","type":"book-chapter","created":{"date-parts":[[2019,8,20]],"date-time":"2019-08-20T16:04:02Z","timestamp":1566317042000},"page":"74-93","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":11,"title":["Restricted Combinatory Unification"],"prefix":"10.1007","author":[{"given":"Ahmed","family":"Bhayat","sequence":"first","affiliation":[]},{"given":"Giles","family":"Reger","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2019,8,20]]},"reference":[{"key":"5_CR1","volume-title":"Term Rewriting and All That","author":"F Baader","year":"1999","unstructured":"Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1999)"},{"key":"5_CR2","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":"5_CR3","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":"5_CR4","doi-asserted-by":"crossref","unstructured":"Bentkamp, A., Blanchette, J.C., Tourret, S., Vukmirovi\u0107, P., Waldmann, U.: Superposition with lambdas (2019, submitted for publication)","DOI":"10.1007\/978-3-030-29436-6_4"},{"key":"5_CR5","unstructured":"Bhayat, A., Reger, G.: Set of support for higher-order reasoning. In: PAAR 2018. CEUR Workshop Proceedings, vol. 2162, pp. 2\u201316 (2018)"},{"key":"5_CR6","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":"5_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1007\/978-3-642-15205-4_15","volume-title":"Computer Science Logic","author":"G Burel","year":"2010","unstructured":"Burel, G.: Embedding deduction modulo into a prover. In: Dawar, A., Veith, H. (eds.) CSL 2010. LNCS, vol. 6247, pp. 155\u2013169. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-15205-4_15"},{"key":"5_CR8","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"},{"issue":"1","key":"5_CR9","doi-asserted-by":"publisher","first-page":"423","DOI":"10.1007\/s10817-018-9458-4","volume":"61","author":"\u0141 Czajka","year":"2018","unstructured":"Czajka, \u0141., Kaliszyk, C.: Hammer for coq: automation for dependent type theory. J. Autom. Reason. 61(1), 423\u2013453 (2018)","journal-title":"J. Autom. Reason."},{"issue":"1","key":"5_CR10","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1016\/j.jal.2006.10.001","volume":"6","author":"FLC de Moura","year":"2008","unstructured":"de Moura, F.L.C., Ayala-Rinc\u00f3n, M., Kamareddine, F.: Higher-order unification: a structural relation between Huet\u2019s method and the one based on explicit substitutions. J. Appl. Logic 6(1), 72\u2013108 (2008)","journal-title":"J. Appl. Logic"},{"issue":"2","key":"5_CR11","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."},{"issue":"1\u20132","key":"5_CR12","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1006\/inco.1999.2837","volume":"157","author":"G Dowek","year":"2000","unstructured":"Dowek, G.: Higher order unification via explicit substitutions. Inf. Comput. 157(1\u20132), 183\u2013235 (2000)","journal-title":"Inf. Comput."},{"issue":"1","key":"5_CR13","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1023\/A:1027357912519","volume":"31","author":"G Dowek","year":"2003","unstructured":"Dowek, G., Hardin, T., Kirchner, C.: Theorem proving modulo. J. Autom. Reason. 31(1), 33\u201372 (2003)","journal-title":"J. Autom. Reason."},{"key":"5_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1007\/3-540-59200-8_52","volume-title":"Rewriting Techniques and Applications","author":"P Graf","year":"1995","unstructured":"Graf, P.: Substitution tree indexing. In: Hsiang, J. (ed.) RTA 1995. LNCS, vol. 914, pp. 117\u2013131. Springer, Heidelberg (1995). https:\/\/doi.org\/10.1007\/3-540-59200-8_52"},{"key":"5_CR15","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"435","DOI":"10.1007\/978-3-642-04617-9_55","volume-title":"KI 2009: Advances in Artificial Intelligence","author":"K Hoder","year":"2009","unstructured":"Hoder, K., Voronkov, A.: Comparing unification algorithms in first-order theorem proving. In: Mertsching, B., Hund, M., Aziz, Z. (eds.) KI 2009. LNCS (LNAI), vol. 5803, pp. 435\u2013443. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-04617-9_55"},{"issue":"1","key":"5_CR16","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1016\/0304-3975(75)90011-0","volume":"1","author":"G Huet","year":"1975","unstructured":"Huet, G.: A unification algorithm for typed $$\\lambda $$-calculus. Theor. Comput. Sci. TCS 1(1), 27\u201357 (1975)","journal-title":"Theor. Comput. Sci. TCS"},{"key":"5_CR17","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":"5_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1007\/BFb0052360","volume-title":"Rewriting Techniques and Applications","author":"J Levy","year":"1998","unstructured":"Levy, J.: Decidable and undecidable second-order unification problems. In: Nipkow, T. (ed.) RTA 1998. LNCS, vol. 1379, pp. 47\u201360. Springer, Heidelberg (1998). https:\/\/doi.org\/10.1007\/BFb0052360"},{"key":"5_CR19","unstructured":"Libal, T., Miller, D.: Functions-as-constructors higher-order unification. In: 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik (2016)"},{"key":"5_CR20","unstructured":"Libal, T., Steen, A.: Towards a substitution tree based index for higher-order resolution theorem provers. In: PAAR 2016. CEUR Workshop Proceedings, vol. 1635 (2016)"},{"issue":"1","key":"5_CR21","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."},{"key":"5_CR22","unstructured":"Miller, D.: Unification of simply typed lambda-terms as logic programming. In: Logic Programming Conference, pp. 255\u2013269. MIT Press (1991)"},{"key":"5_CR23","unstructured":"Paulson, L.C., Blanchette, J.C.: Three years of experience with sledgehammer, a practical link between automatic and interactive theorem provers. In: IWIL 2010, vol. 2, pp. 1\u201311 (2010)"},{"issue":"1","key":"5_CR24","doi-asserted-by":"publisher","first-page":"6:1","DOI":"10.1145\/1614431.1614437","volume":"11","author":"B Pientka","year":"2009","unstructured":"Pientka, B.: Higher-order term indexing using substitution trees. ACM Trans. Comput. Logic 11(1), 6:1\u20136:40 (2009)","journal-title":"ACM Trans. Comput. Logic"},{"key":"5_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"635","DOI":"10.1007\/3-540-58156-1_46","volume-title":"Automated Deduction \u2014 CADE-12","author":"C Prehofer","year":"1994","unstructured":"Prehofer, C.: Decidable higher-order unification problems. In: Bundy, A. (ed.) CADE 1994. LNCS, vol. 814, pp. 635\u2013649. Springer, Heidelberg (1994). https:\/\/doi.org\/10.1007\/3-540-58156-1_46"},{"issue":"2","key":"5_CR26","doi-asserted-by":"publisher","first-page":"905","DOI":"10.1016\/j.jsc.2005.01.005","volume":"40","author":"M Schmidt-Schau\u00df","year":"2005","unstructured":"Schmidt-Schau\u00df, M., Schulz, K.U.: Decidability of bounded higher-order unification. J. Symb. Comput. 40(2), 905\u2013954 (2005)","journal-title":"J. Symb. Comput."},{"issue":"1\u20132","key":"5_CR27","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.: Higher-order unification revisited: complete sets of transformations. J. Symb. Comput. 8(1\u20132), 101\u2013140 (1989)","journal-title":"J. Symb. Comput."},{"key":"5_CR28","doi-asserted-by":"crossref","unstructured":"Steen, A.: Extensional Paramodulation for Higher-Order Logic and its Effective Implementation Leo-III. Ph.D. thesis, Freie Universit\u00e4t Berlin (2018)","DOI":"10.1007\/s13218-019-00628-8"},{"key":"5_CR29","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"},{"key":"5_CR30","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":"4","key":"5_CR31","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":"5_CR32","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"}],"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_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,7,11]],"date-time":"2022-07-11T21:53:56Z","timestamp":1657576436000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-29436-6_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030294359","9783030294366"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-29436-6_5","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"}}]}}