{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T13:36:47Z","timestamp":1725543407077},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540368342"},{"type":"electronic","value":"9783540368359"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11805618_16","type":"book-chapter","created":{"date-parts":[[2006,7,25]],"date-time":"2006-07-25T14:29:13Z","timestamp":1153837753000},"page":"212-226","source":"Crossref","is-referenced-by-count":9,"title":["Checking Conservativity of Overloaded Definitions in Higher-Order Logic"],"prefix":"10.1007","author":[{"given":"Steven","family":"Obua","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"16_CR1","unstructured":"Obua, S.: Conservative Overloading in Higher-Order Logic. Technical Report, Institut f\u00fcr Informatik, Technische Universit\u00e4t M\u00fcnchen (2006), \n                    \n                      http:\/\/www4.in.tum.de\/~obua\/checkdefs"},{"issue":"3","key":"16_CR2","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1007\/BF00248324","volume":"5","author":"L.C. Paulson","year":"1989","unstructured":"Paulson, L.C.: The Foundation of a Generic Theorem Prover. Journal of Automated Reasoning\u00a05(3), 363\u2013397 (1989)","journal-title":"Journal of Automated Reasoning"},{"key":"16_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1007\/BFb0028402","volume-title":"Theorem Proving in Higher Order Logics","author":"M. Wenzel","year":"1997","unstructured":"Wenzel, M.: Type Classes and Overloading in Higher-Order Logic. In: Gunter, E.L., Felty, A.P. (eds.) TPHOLs 1997. LNCS, vol.\u00a01275, pp. 307\u2013322. Springer, Heidelberg (1997)"},{"key":"16_CR4","doi-asserted-by":"crossref","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. Springer, Heidelberg (2002)"},{"key":"16_CR5","doi-asserted-by":"crossref","unstructured":"Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge U.P., NewYork (1998)","DOI":"10.1017\/CBO9781139172752"},{"key":"16_CR6","unstructured":"Terese: Term Rewriting Systems. Cambridge U.P., New York (2003)"},{"key":"16_CR7","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1016\/S0304-3975(99)00207-8","volume":"236","author":"T. Arts","year":"2000","unstructured":"Arts, T., Giesl, J.: Termination of term rewriting using dependency pairs. Theoretical Computer Science\u00a0236, 133\u2013178 (2000)","journal-title":"Theoretical Computer Science"},{"key":"16_CR8","doi-asserted-by":"publisher","first-page":"172","DOI":"10.1016\/j.ic.2004.10.004","volume":"199","author":"N. Hirokawa","year":"2005","unstructured":"Hirokawa, N., Middeldorp, A.: Automating the dependency pair method. Information and Computation\u00a0199, 172\u2013199 (2005)","journal-title":"Information and Computation"},{"issue":"12","key":"16_CR9","first-page":"579","volume":"21","author":"K. Ruohonen","year":"1985","unstructured":"Ruohonen, K.: Reversible Machines and Post\u2019s Correspondence Problem for Biprefix Morphisms. Journal of Information Processing and Cybernetics\u00a021(12), 579\u2013595 (1985)","journal-title":"Journal of Information Processing and Cybernetics"},{"key":"16_CR10","unstructured":"The HOL System Description, \n                    \n                      http:\/\/hol.sourceforge.net\/"},{"key":"16_CR11","unstructured":"Harrison, J.: The HOL Light theorem prover, \n                    \n                      http:\/\/www.cl.cam.ac.uk\/~jrh\/hol-light\/"},{"key":"16_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"210","DOI":"10.1007\/978-3-540-25979-4_15","volume-title":"Rewriting Techniques and Applications","author":"J. Giesl","year":"2004","unstructured":"Giesl, J., Thiemann, R., Schneider-Kamp, P., Falke, S.: Automated Termination Proofs with AProVE. In: van Oostrom, V. (ed.) RTA 2004. LNCS, vol.\u00a03091, pp. 210\u2013220. Springer, Heidelberg (2004), \n                    \n                      http:\/\/www-i2.informatik.rwth-aachen.de\/AProVE\/"},{"key":"16_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/978-3-540-32033-3_14","volume-title":"Term Rewriting and Applications","author":"N. Hirokawa","year":"2005","unstructured":"Hirokawa, N., Middeldorp, A.: Tyrolean Termination Tool. In: Giesl, J. (ed.) RTA 2005. LNCS, vol.\u00a03467, pp. 175\u2013184. Springer, Heidelberg (2005), \n                    \n                      http:\/\/cl2-informatik.uibk.ac.at\/ttt\/"},{"key":"16_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"227","DOI":"10.1007\/11541868_15","volume-title":"Theorem Proving in Higher Order Logics","author":"S. Obua","year":"2005","unstructured":"Obua, S.: Proving Bounds for Real Linear Programs in Isabelle\/HOL. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol.\u00a03603, pp. 227\u2013244. Springer, Heidelberg (2005)"},{"key":"16_CR15","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1007\/11532231_4","volume-title":"Automated Deduction \u2013 CADE-20","author":"C. Urban","year":"2005","unstructured":"Urban, C.: Nominal Techniques in Isabelle\/HOL. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol.\u00a03632, pp. 38\u201353. Springer, Heidelberg (2005)"},{"key":"16_CR16","unstructured":"Project Bali, \n                    \n                      http:\/\/isabelle.in.tum.de\/Bali"},{"key":"16_CR17","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4757-5662-3","volume-title":"Linear Programming","author":"R.J. Vanderbei","year":"2001","unstructured":"Vanderbei, R.J.: Linear Programming, 2nd edn. Springer, Heidelberg (2001)","edition":"2"},{"key":"16_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"426","DOI":"10.1007\/3-540-59200-8_77","volume-title":"Rewriting Techniques and Applications","author":"J. Giesl","year":"1995","unstructured":"Giesl, J.: Generating Polynomial Orderings for Termination Proofs. In: Hsiang, J. (ed.) RTA 1995. LNCS, vol.\u00a0914, pp. 426\u2013431. Springer, Heidelberg (1995)"},{"key":"16_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1007\/3-540-45685-6_8","volume-title":"Theorem Proving in Higher Order Logics","author":"A.D. Brucker","year":"2002","unstructured":"Brucker, A.D., Wolff, B.: A Proposal for a Formal OCL Semantics in Isabelle\/HOL. In: Carre\u00f1o, V.A., Mu\u00f1oz, C.A., Tahar, S. (eds.) TPHOLs 2002. LNCS, vol.\u00a02410, pp. 99\u2013114. Springer, Heidelberg (2002)"},{"key":"16_CR20","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/s002000100063","volume":"12","author":"J. Giesl","year":"2001","unstructured":"Giesl, J., Arts, T.: Verification of Erlang Processes by Dependency Pairs. Applicable Algebra in Engineering, Communication and Computing\u00a012, 39\u201372 (2001)","journal-title":"Applicable Algebra in Engineering, Communication and Computing"}],"container-title":["Lecture Notes in Computer Science","Term Rewriting and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11805618_16.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T07:26:00Z","timestamp":1619508360000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11805618_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540368342","9783540368359"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/11805618_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}