{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T16:31:53Z","timestamp":1725467513503},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540649878"},{"type":"electronic","value":"9783540498018"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/bfb0055142","type":"book-chapter","created":{"date-parts":[[2006,7,27]],"date-time":"2006-07-27T09:09:13Z","timestamp":1153991353000},"page":"277-293","source":"Crossref","is-referenced-by-count":6,"title":["An LPO-based termination ordering for higher-order terms without \u03bb-abstraction"],"prefix":"10.1007","author":[{"given":"Maxim","family":"Lifantsev","sequence":"first","affiliation":[]},{"given":"Leo","family":"Bachmair","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2006,5,27]]},"reference":[{"issue":"2","key":"17_CR1","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1016\/0304-3975(94)00275-4","volume":"142","author":"N. Dershowitz","year":"1995","unstructured":"Nachum Dershowitz and Charles Hoot. Natural termination. Theoretical Computer Science, 142(2):179\u2013207, May 1995.","journal-title":"Theoretical Computer Science"},{"key":"17_CR2","first-page":"243","volume-title":"Handbook of Theoretical Computer Science, volume B: Formal Methods and Semantics","author":"N. Dershowitz","year":"1990","unstructured":"Nachum Dershowitz and Jean-Pierre Jouannaud. Rewrite systems. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B: Formal Methods and Semantics, chapter 6, pages 243\u2013320. North-Holland, Amsterdam, 1990."},{"key":"17_CR3","unstructured":"Stephen J. Garland and John V. Guttag. LP, the Larch Prover: Version 3.1. MIT Laboratory for Computer Science, January 1995. Available electronically at http:\/\/larch.lcs.mit.edu:8001\/larch\/LP\/overview.html."},{"key":"17_CR4","first-page":"108","volume-title":"volume 1103 of Lecture Notes in Computer Science","author":"J. Jouannaud","year":"1996","unstructured":"Jean-Pierre Jouannaud and Albert Rubio. A recursive path ordering for higher-order terms in \u03b7-long \u0392-normal form. In Harald Ganzinger, editor, Proceedings of the 7th International Conference on Rewriting Techniques and Applications (RTA-96), volume 1103 of Lecture Notes in Computer Science, pages 108\u2013122, New Brunswick, NJ, USA, July 27\u201330 1996. Springer-Verlag."},{"key":"17_CR5","doi-asserted-by":"crossref","unstructured":"Jean-Pierre Jouannaud and Albert Rubio. Rewrite orderings for higher-order terms in \u03b7-long \u0392-normal form and the recursive path ordering. To appear in Theoretical Computer Science, 1998. Available also at http:\/\/www-lsi.upc.es\/~albert\/papers\/horpo.ps.gz.","DOI":"10.1016\/S0304-3975(98)00078-4"},{"key":"17_CR6","first-page":"241","volume-title":"volume 914 of Lecture Notes in Computer Science","author":"S. Kahrs","year":"1995","unstructured":"Stefan Kahrs. Towards a domain theory for termination proofs. In Jieh Hsiang, editor, Proceedings of the 6th International Conference on Rewriting Techniques and Applications (RTA-95), volume 914 of Lecture Notes in Computer Science, pages 241\u2013255, Kaiserslautern, Germany, April 5\u20137 1995. Springer-Verlag."},{"key":"17_CR7","volume-title":"Diploma thesis","author":"M. Lifantsev","year":"1996","unstructured":"Maxim Lifantsev. Term rewriting systems. Diploma thesis, Moscow State Engineering-Physics Institute (Technical University), Moscow, Russia, February 1996. In Russian."},{"key":"17_CR8","doi-asserted-by":"crossref","unstructured":"Carlos Loria-Saenz and Joachim Steinbach. Termination of combined (rewrite and \u03bb-calculus) systems. In Micha\u00cbl Rusinowitch and Jean-Luc R\u00e9my, editors, Conditional Term Rewriting Systems, Third International Workshop, volume 656 of Lecture Notes in Computer Science, pages 143\u2013147, Pont-\u00e0-Mousson, France, July 8\u201310, 1992. Springer-Verlag.","DOI":"10.1007\/3-540-56393-8_10"},{"key":"17_CR9","first-page":"26","volume-title":"volume 914 of Lecture Notes in Computer Science","author":"O. Lysne","year":"1995","unstructured":"Olav Lysne and Javier Piris. A termination ordering for higher order rewrite systems. In Jieh Hsiang, editor, Proceedings of the 6th International Conference on Rewriting Techniques and Applications (RTA-95), volume 914 of Lecture Notes in Computer Science, pages 26\u201340, Kaiserslautern, Germany, April 5\u20137 1995. Springer-Verlag."},{"key":"17_CR10","unstructured":"M.J.C. Gordon and T.F. Melham. Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Cambridge University Press, 1993."},{"key":"17_CR11","volume-title":"Technical Report SRI-CSL-97-2","author":"S. Owre","year":"1997","unstructured":"Sam Owre and Natarajan Shankar. The formal semantics of PVS. Technical Report SRI-CSL-97-2, Computer Science Laboratory, SRI International, Menlo Park, CA, August 1997."},{"key":"17_CR12","unstructured":"Lawrence C. Paulson. Introduction to Isabelle. Technical Report 280, University of Cambridge, Computer Laboratory, 1993."},{"key":"17_CR13","first-page":"350","volume-title":"volume 816 of Lecture Notes in Computer Science","author":"J. Pol Van de","year":"1993","unstructured":"Jaco Van de Pol. Termination proofs for higher-order rewrite systems. In J. Heering, K. Meinke, B. Moeller, and T. Nipkow, editors, Higher-Order Algebra, Logic, and Term Rewriting, First International Workshop, volume 816 of Lecture Notes in Computer Science, pages 350\u2013325, Amsterdam, The Netherlands, September 1993. Springer-Verlag."},{"key":"17_CR14","first-page":"350","volume-title":"volume 902 of Lecture Notes in Computer Science","author":"J. Pol Van de","year":"1995","unstructured":"Jaco Van de Pol and Helmut Schwichtenberg. Strict functionals for termination proofs. In M. Dezani-Ciancaglini and G. Plotkin, editors, Proceedings of the International Conference on Typed Lambda Calculi and Applications, volume 902 of Lecture Notes in Computer Science, pages 350\u2013364, Edinburgh, Scotland, April 1995. Springer-Verlag."}],"container-title":["Lecture Notes in Computer Science","Theorem Proving in Higher Order Logics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0055142","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,20]],"date-time":"2019-04-20T08:34:19Z","timestamp":1555749259000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0055142"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540649878","9783540498018"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/bfb0055142","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1998]]}}}