{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T17:36:40Z","timestamp":1725903400016},"publisher-location":"Cham","reference-count":51,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319630458"},{"type":"electronic","value":"9783319630465"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-63046-5_27","type":"book-chapter","created":{"date-parts":[[2017,7,10]],"date-time":"2017-07-10T09:34:07Z","timestamp":1499679247000},"page":"432-453","source":"Crossref","is-referenced-by-count":12,"title":["A Transfinite Knuth\u2013Bendix Order for Lambda-Free Higher-Order Terms"],"prefix":"10.1007","author":[{"given":"Heiko","family":"Becker","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jasmin Christian","family":"Blanchette","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Uwe","family":"Waldmann","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Daniel","family":"Wand","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,7,11]]},"reference":[{"unstructured":"Andrews, P.B., Cohen, E.L.: Theorem proving in type theory. In: Reddy, R. (ed.) IJCAI 1977, p. 566. William Kaufmann (1977)","key":"27_CR1"},{"key":"27_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"380","DOI":"10.1007\/3-540-44881-0_27","volume-title":"Rewriting Techniques and Applications","author":"T Aoto","year":"2003","unstructured":"Aoto, T., Yamada, T.: Termination of simply typed term rewriting by translation and labelling. In: Nieuwenhuis, R. (ed.) RTA 2003. LNCS, vol. 2706, pp. 380\u2013394. Springer, Heidelberg (2003). doi: 10.1007\/3-540-44881-0_27"},{"key":"27_CR3","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781139172752","volume-title":"Term Rewriting and All That","author":"F Baader","year":"1998","unstructured":"Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998)"},{"issue":"4","key":"27_CR4","doi-asserted-by":"crossref","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. Reasoning 47(4), 451\u2013479 (2011)","journal-title":"J. Autom. Reasoning"},{"issue":"4","key":"27_CR5","doi-asserted-by":"crossref","first-page":"557","DOI":"10.1017\/S0960129506005317","volume":"16","author":"J-P Ban\u00e2tre","year":"2006","unstructured":"Ban\u00e2tre, J.-P., Fradet, P., Radenac, Y.: Generalised multisets for chemical programming. Math. Struct. Comput. Sci. 16(4), 557\u2013580 (2006)","journal-title":"Math. Struct. Comput. Sci."},{"unstructured":"Becker, H., Blanchette, J.C., Waldmann, U., Wand, D.: Formalization of Knuth-Bendix orders for lambda-free higher-order terms. Archive of Formal Proofs (2016). Formal proof development, https:\/\/isa-afp.org\/entries\/Lambda_Free_KBOs.shtml","key":"27_CR6"},{"doi-asserted-by":"crossref","unstructured":"Becker, H., Blanchette, J.C., Waldmann, U., Wand, D.: Transfinite Knuth-Bendix orders for lambda-free higher-order terms. Tech. report (2017), http:\/\/cs.vu.nl\/~jbe248\/lambda_free_kbo_rep.pdf","key":"27_CR7","DOI":"10.1007\/978-3-319-63046-5_27"},{"key":"27_CR8","series-title":"Lecture Notes in Computer Science","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, vol. 3097, pp. 460\u2013474. Springer, Heidelberg (2004). doi: 10.1007\/978-3-540-25984-8_34"},{"key":"27_CR9","series-title":"Lecture Notes in Computer Science","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, vol. 1421, pp. 56\u201371. Springer, Heidelberg (1998). doi: 10.1007\/BFb0054248"},{"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)","key":"27_CR10","DOI":"10.1016\/B978-0-444-51624-4.50005-8"},{"unstructured":"Blanchette, J.C., Fleury, M., Traytel, D.: Formalization of nested multisets, hereditary multisets, and syntactic ordinals. Archive of Formal Proofs (2016). Formal proof development, https:\/\/isa-afp.org\/entries\/Nested_Multisets_Ordinals.shtml","key":"27_CR11"},{"key":"27_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/978-3-319-08970-6_7","volume-title":"Interactive Theorem Proving","author":"JC Blanchette","year":"2014","unstructured":"Blanchette, J.C., H\u00f6lzl, J., Lochbihler, A., Panny, L., Popescu, A., Traytel, D.: Truly modular (Co)datatypes for Isabelle\/HOL. In: Klein, G., Gamboa, R. (eds.) ITP 2014. LNCS, vol. 8558, pp. 93\u2013110. Springer, Cham (2014). doi: 10.1007\/978-3-319-08970-6_7"},{"issue":"1","key":"27_CR13","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. Formalized Reasoning 9(1), 101\u2013148 (2016)","journal-title":"J. Formalized Reasoning"},{"key":"27_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1007\/978-3-642-14052-5_11","volume-title":"Interactive Theorem Proving","author":"JC Blanchette","year":"2010","unstructured":"Blanchette, J.C., Nipkow, T.: Nitpick: a counterexample generator for higher-order logic based on a relational model finder. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 131\u2013146. Springer, Heidelberg (2010). doi: 10.1007\/978-3-642-14052-5_11"},{"unstructured":"Blanchette, J.C., Waldmann, U., Wand, D.: Formalization of recursive path orders for lambda-free higher-order terms. Archive of Formal Proofs (2016). Formal proof development, https:\/\/isa-afp.org\/entries\/Lambda_Free_RPOs.shtml","key":"27_CR15"},{"key":"27_CR16","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\u00a0path\u00a0order. In: Esparza, J., Murawski, A.S. (eds.) FoSSaCS 2017. LNCS, vol. 10203, pp. 461\u2013479. Springer, Heidelberg (2017). doi: 10.1007\/978-3-662-54458-7_27"},{"doi-asserted-by":"crossref","unstructured":"Blanqui, F., Jouannaud, J.-P., Rubio, A.: The computability path ordering. Log. Meth. Comput. Sci. 11(4) (2015)","key":"27_CR17","DOI":"10.2168\/LMCS-11(4:3)2015"},{"issue":"1","key":"27_CR18","doi-asserted-by":"crossref","first-page":"263","DOI":"10.1093\/logcom\/exs027","volume":"23","author":"M Bofill","year":"2013","unstructured":"Bofill, M., Borralleras, C., Rodr\u00edguez-Carbonell, E., Rubio, A.: The recursive path and polynomial ordering for first-order and higher-order terms. J. Log. Comput. 23(1), 263\u2013305 (2013)","journal-title":"J. Log. Comput."},{"issue":"1","key":"27_CR19","doi-asserted-by":"crossref","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. Reasoning 50(1), 51\u201398 (2013)","journal-title":"J. Autom. Reasoning"},{"issue":"8","key":"27_CR20","doi-asserted-by":"crossref","first-page":"465","DOI":"10.1145\/359138.359142","volume":"22","author":"N Dershowitz","year":"1979","unstructured":"Dershowitz, N., Manna, Z.: Proving termination with multiset orderings. Commun. ACM 22(8), 465\u2013476 (1979)","journal-title":"Commun. ACM"},{"key":"27_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"106","DOI":"10.1007\/3-540-60381-6_7","volume-title":"Conditional and Typed Rewriting Systems","author":"MCF Ferreira","year":"1995","unstructured":"Ferreira, M.C.F., Zantema, H.: Well-foundedness of term orderings. In: Dershowitz, N., Lindenstrauss, N. (eds.) CTRS 1994. LNCS, vol. 968, pp. 106\u2013123. Springer, Heidelberg (1995). doi: 10.1007\/3-540-60381-6_7"},{"key":"27_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"216","DOI":"10.1007\/11559306_12","volume-title":"Frontiers of Combining Systems","author":"J Giesl","year":"2005","unstructured":"Giesl, J., Thiemann, R., Schneider-Kamp, P.: Proving and disproving termination of higher-order functions. In: Gramlich, B. (ed.) FroCoS 2005. LNCS, vol. 3717, pp. 216\u2013231. Springer, Heidelberg (2005). doi: 10.1007\/11559306_12"},{"issue":"2","key":"27_CR23","doi-asserted-by":"crossref","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."},{"issue":"3","key":"27_CR24","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1007\/s10817-012-9248-3","volume":"50","author":"N Hirokawa","year":"2013","unstructured":"Hirokawa, N., Middeldorp, A., Zankl, H.: Uncurrying for termination and complexity. J. Autom. Reasoning 50(3), 279\u2013315 (2013)","journal-title":"J. Autom. Reasoning"},{"doi-asserted-by":"crossref","unstructured":"Huet, G., Oppen, D.C.: Equations and rewrite rules: a survey. In: Book, R.V. (ed.) Formal Language Theory: Perspectives and Open Problems, pp. 349\u2013405. Academic Press (1980)","key":"27_CR25","DOI":"10.1016\/B978-0-12-115350-2.50017-8"},{"unstructured":"Huet, G.P.: A mechanization of type theory. In: Nilsson, N.J. (ed.) International Joint Conference on Artificial Intelligence (IJCAI 1973), pp. 139\u2013146. William Kaufmann (1973)","key":"27_CR26"},{"doi-asserted-by":"crossref","unstructured":"Hughes, R.J.M.: Super-combinators: a new implementation method for applicative languages. In: LFP 1982, pp. 1\u201310. ACM Press (1982)","key":"27_CR27","DOI":"10.1145\/800068.802129"},{"issue":"1","key":"27_CR28","first-page":"2:1","volume":"54","author":"J-P 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"},{"issue":"1","key":"27_CR29","doi-asserted-by":"crossref","first-page":"15","DOI":"10.1006\/jsco.1996.0002","volume":"21","author":"R Kennaway","year":"1996","unstructured":"Kennaway, R., Klop, J.W., Sleep, M.R., de Vries, F.: Comparing curried and uncurried rewriting. J. Symbolic Comput. 21(1), 15\u201339 (1996)","journal-title":"J. Symbolic Comput."},{"doi-asserted-by":"crossref","unstructured":"Knuth, D.E., Bendix, P.B.: Simple word problems in universal algebras. In: Leech, J. (ed.) Computational Problems in Abstract Algebra, pp. 263\u2013297. Pergamon Press (1970)","key":"27_CR30","DOI":"10.1016\/B978-0-08-012975-4.50028-X"},{"unstructured":"Kop, C.: Higher Order Termination. Ph.D. thesis, Vrije Universiteit Amsterdam (2012)","key":"27_CR31"},{"key":"27_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"697","DOI":"10.1007\/978-3-540-89439-1_48","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"C Kop","year":"2008","unstructured":"Kop, C., Raamsdonk, F.: A higher-order iterative path ordering. In: Cervesato, I., Veith, H., Voronkov, A. (eds.) LPAR 2008. LNCS, vol. 5330, pp. 697\u2013711. Springer, Heidelberg (2008). doi: 10.1007\/978-3-540-89439-1_48"},{"key":"27_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"384","DOI":"10.1007\/978-3-642-22438-6_29","volume-title":"Automated Deduction \u2013 CADE-23","author":"L Kov\u00e1cs","year":"2011","unstructured":"Kov\u00e1cs, L., Moser, G., Voronkov, A.: On transfinite Knuth-Bendix orders. In: Bj\u00f8rner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS, vol. 6803, pp. 384\u2013399. Springer, Heidelberg (2011). doi: 10.1007\/978-3-642-22438-6_29"},{"key":"27_CR34","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). doi: 10.1007\/978-3-642-39799-8_1"},{"key":"27_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"277","DOI":"10.1007\/BFb0055142","volume-title":"Theorem Proving in Higher Order Logics","author":"M Lifantsev","year":"1998","unstructured":"Lifantsev, M., Bachmair, L.: An LPO-based termination ordering for higher-order terms without $$\\lambda $$ -abstraction. In: Grundy, J., Newey, M. (eds.) TPHOLs 1998. LNCS, vol. 1479, pp. 277\u2013293. Springer, Heidelberg (1998). doi: 10.1007\/BFb0055142"},{"issue":"4","key":"27_CR36","doi-asserted-by":"crossref","first-page":"289","DOI":"10.1007\/s10817-006-9031-4","volume":"36","author":"B L\u00f6chner","year":"2006","unstructured":"L\u00f6chner, B.: Things to know when implementing KBO. J. Autom. Reasoning 36(4), 289\u2013310 (2006)","journal-title":"J. Autom. Reasoning"},{"key":"27_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1007\/978-3-540-75560-9_26","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"M Ludwig","year":"2007","unstructured":"Ludwig, M., Waldmann, U.: An extension of the Knuth-Bendix ordering with LPO-like properties. In: Dershowitz, N., Voronkov, A. (eds.) LPAR 2007. LNCS, vol. 4790, pp. 348\u2013362. Springer, Heidelberg (2007). doi: 10.1007\/978-3-540-75560-9_26"},{"doi-asserted-by":"crossref","unstructured":"McCune, W.: Otter 3.3 reference manual. Technical. Report 263 (2003)","key":"27_CR38","DOI":"10.2172\/822573"},{"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)","key":"27_CR39","DOI":"10.1016\/B978-044450813-3\/50009-6"},{"key":"27_CR40","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","year":"2002","unstructured":"Nipkow, T., Wenzel, M., Paulson, L.C. (eds.): Isabelle\/HOL: A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002). doi: 10.1007\/3-540-45949-9"},{"key":"27_CR41","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\u00a01.8. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds.) LPAR 2013. LNCS, vol. 8312, pp. 735\u2013743. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-45221-5_49"},{"unstructured":"Sternagel, C., Thiemann, R.: Executable multivariate polynomials. Archive of Formal Proofs (2010). Formal proof development, https:\/\/isa-afp.org\/entries\/Polynomials.shtml","key":"27_CR42"},{"key":"27_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1007\/978-3-642-24364-6_17","volume-title":"Frontiers of Combining Systems","author":"C Sternagel","year":"2011","unstructured":"Sternagel, C., Thiemann, R.: Generalized and formalized uncurrying. In: Tinelli, C., Sofronie-Stokkermans, V. (eds.) FroCoS 2011. LNCS, vol. 6989, pp. 243\u2013258. Springer, Heidelberg (2011). doi: 10.1007\/978-3-642-24364-6_17"},{"unstructured":"Sternagel, C., Thiemann, R.: Formalizing Knuth-Bendix orders and Knuth-Bendix completion. In: van Raamsdonk, F. (ed.) RTA 2013, vol. 21. LIPIcs, pp. 287\u2013302. Schloss Dagstuhl (2013)","key":"27_CR44"},{"issue":"1","key":"27_CR45","doi-asserted-by":"crossref","first-page":"91","DOI":"10.1016\/j.jal.2012.12.002","volume":"11","author":"N Sultana","year":"2013","unstructured":"Sultana, N., Blanchette, J.C., Paulson, L.C.: LEO-II and Satallax on the Sledgehammer test bench. J. Applied Logic 11(1), 91\u2013102 (2013)","journal-title":"J. Applied Logic"},{"key":"27_CR46","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"40","DOI":"10.1007\/978-3-540-25979-4_3","volume-title":"Rewriting Techniques and Applications","author":"Y Toyama","year":"2004","unstructured":"Toyama, Y.: Termination of S-expression rewriting systems: lexicographic path ordering for higher-order terms. In: Oostrom, V. (ed.) RTA 2004. LNCS, vol. 3091, pp. 40\u201354. Springer, Heidelberg (2004). doi: 10.1007\/978-3-540-25979-4_3"},{"issue":"1","key":"27_CR47","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1002\/spe.4380090105","volume":"9","author":"DA Turner","year":"1979","unstructured":"Turner, D.A.: A new implementation technique for applicative languages. Softw. Pract. Experience 9(1), 31\u201349 (1979)","journal-title":"Softw. Pract. Experience"},{"key":"27_CR48","series-title":"Lecture Notes in Computer Science","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, vol. 5663, pp. 140\u2013145. Springer, Heidelberg (2009). doi: 10.1007\/978-3-642-02959-2_10"},{"key":"27_CR49","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"362","DOI":"10.1007\/978-3-319-40229-1_25","volume-title":"Automated Reasoning","author":"M Wisniewski","year":"2016","unstructured":"Wisniewski, M., Steen, A., Kern, K., Benzm\u00fcller, C.: Effective normalization techniques for HOL. In: Olivetti, N., Tiwari, A. (eds.) IJCAR 2016. LNCS, vol. 9706, pp. 362\u2013370. Springer, Cham (2016). doi: 10.1007\/978-3-319-40229-1_25"},{"key":"27_CR50","doi-asserted-by":"crossref","first-page":"129","DOI":"10.1016\/j.jsc.2014.09.033","volume":"69","author":"H Zankl","year":"2015","unstructured":"Zankl, H., Winkler, S., Middeldorp, A.: Beyond polynomials and Peano arithmetic\u2013automation of elementary and ordinal interpretations. J. Symb. Comput. 69, 129\u2013158 (2015)","journal-title":"J. Symb. Comput."},{"unstructured":"Zantema, H.: Termination. In: Bezem, M., Klop, J.W., de Vrijer, R. (eds.) Term Rewriting Systems. Cambridge Tracts in Theoretical Computer Science, vol. 55, pp. 181\u2013259. Cambridge University Press, Cambridge (2003)","key":"27_CR51"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE 26"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-63046-5_27","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,29]],"date-time":"2019-09-29T04:28:46Z","timestamp":1569731326000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-63046-5_27"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319630458","9783319630465"],"references-count":51,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-63046-5_27","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}