{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:22:53Z","timestamp":1725664973762},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540617396"},{"type":"electronic","value":"9783540706748"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/3-540-61739-6_44","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T22:19:00Z","timestamp":1330294740000},"page":"220-237","source":"Crossref","is-referenced-by-count":1,"title":["Automated modular termination proofs for real Prolog programs"],"prefix":"10.1007","author":[{"given":"Martin","family":"M\u00fcller","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thomas","family":"Gla\u00df","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Karl","family":"Stroetmann","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,2]]},"reference":[{"key":"16_CR1","doi-asserted-by":"crossref","first-page":"743","DOI":"10.1007\/BF01213601","volume":"6A","author":"K. R. Apt","year":"1994","unstructured":"Krzysztof R. Apt and Elena Marchiori. Reasoning about Prolog programs: From modes through types to assertions. Formal Aspects of Computing, 6A:743\u2013764, 1994.","journal-title":"Formal Aspects of Computing"},{"key":"16_CR2","doi-asserted-by":"crossref","unstructured":"Krzysztof R. Apt and Dino Pedreschi. Studies in pure Prolog: Termination. In John W. Lloyd, editor, Symposium on Computational Logic, pages 150\u2013176. Springer-Verlag, 1990.","DOI":"10.1007\/978-3-642-76274-1_9"},{"key":"16_CR3","unstructured":"Krysztof R. Apt and Dino Pedreschi. Modular termination proofs for logic and pure prolog programs. In G. Levi, editor, Proceedings of Fourth International School for Computer Science Researchers. Oxford University Press, 1993."},{"volume-title":"Proceedings of the Joint International Conference and Symposium on Logic Programming","year":"1992","key":"16_CR4","unstructured":"Krzysztof R. Apt, editor. Proceedings of the Joint International Conference and Symposium on Logic Programming, Washington, D. C., USA, November, 9\u201313 1992. The MIT Press."},{"key":"16_CR5","doi-asserted-by":"crossref","unstructured":"J\u00fcrgen Avenhaus. Reduktionssysteme \u2014 Rechnen und Schlie\u0392en in gleichungsdefinierten Strukturen, Springer-Verlag, 1995.","DOI":"10.1007\/978-3-642-79351-6"},{"key":"16_CR6","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4684-7118-2","volume-title":"Canonical Equational Proofs","author":"L. Bachmair","year":"1991","unstructured":"Leo Bachmair. Canonical Equational Proofs. Birkh\u00e4user Boston, Inc., Boston, MA, 1991."},{"issue":"2","key":"16_CR7","doi-asserted-by":"crossref","first-page":"297","DOI":"10.1016\/0304-3975(92)00019-N","volume":"124","author":"Bossi","year":"1994","unstructured":"Bossi, Coco, and Fabris. Norms on terms and their use in proving universal termination of a logic program. Theoretical Computer Science, 124,2:297\u2013328, 1994.","journal-title":"Theoretical Computer Science"},{"key":"16_CR8","first-page":"69","volume-title":"Characterizing termination of logic programs with level mappings","author":"M. Bezem","year":"1989","unstructured":"Marc Bezem. Characterizing termination of logic programs with level mappings. In Ewing L. Lusk and Ross A. Qverbeek, editors, Logic Programming, Proceedings of the North American Conference, volume 1, pages 69\u201380, Cleveland, Ohio, USA, October 16\u201320, 1989. The MIT Press, Cambridge, Massachusetts."},{"issue":"1","key":"16_CR9","doi-asserted-by":"crossref","first-page":"79","DOI":"10.1016\/0743-1066(93)90014-8","volume":"15","author":"M. Bezem","year":"1993","unstructured":"Marc Bezem. Strong termination of logic programs. Journal of Logic Programming, 15(1&2):79\u201398, 1993.","journal-title":"Journal of Logic Programming"},{"key":"16_CR10","unstructured":"W. W. Bledsoe. A new method for proving Presburger formulas. In 4th International Joint Conference on Artificial Intelligence, September 1975. Tibilisi, Georgia, U.S.S.R."},{"key":"16_CR11","first-page":"321","volume-title":"A framework of directionality for proving termination of logic programs","author":"F. Bronsard","year":"1992","unstructured":"Fran\u00c7ois Bronsard, T. K. Lakshman, and Uday S. Reddy. A framework of directionality for proving termination of logic programs. In Apt [Apt92], pages 321\u2013335."},{"key":"16_CR12","doi-asserted-by":"crossref","first-page":"293","DOI":"10.1007\/978-1-4684-3384-5_11","volume-title":"Logic and Data Bases","author":"K. L. Clark","year":"1978","unstructured":"K. L. Clark. Negation as failure. In H. Gallaire and J. Minker, editors, Logic and Data Bases, pages 293\u2013322. Plenum Press, New York, 1978."},{"key":"16_CR13","doi-asserted-by":"crossref","unstructured":"P. Deransart, A. A. Ed-Dbali, and L. Cervoni. Prolog: The Standard. Springer-Verlag, 1996.","DOI":"10.1007\/978-3-642-61411-8"},{"key":"16_CR14","unstructured":"Herbert B. Enderton. A Mathematical Introduction to Logic. Academic Press, 1972."},{"key":"16_CR15","first-page":"336","volume-title":"Handling of mutual recursion in automatic termination proofs for logic programs","author":"G. Gr\u00f6ger","year":"1992","unstructured":"Gerhard Gr\u00f6ger and Lutz Pl\u00fcmer. Handling of mutual recursion in automatic termination proofs for logic programs. In Apt [Apt92], pages 336\u2013350."},{"key":"16_CR16","first-page":"1","volume-title":"Types in Logic Programming","author":"P. M. Hill","year":"1992","unstructured":"P. M. Hill and R. W. Topor. A semantics for typed logic programs. In Pfenning [Pfe92], pages 1\u201362."},{"key":"16_CR17","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-83189-8","volume-title":"Foundations of Logic Programming","author":"J. W. Lloyd","year":"1987","unstructured":"J. W. Lloyd. Foundations of Logic Programming. Springer-Verlag, Berlin, second edition, 1987.","edition":"second edition"},{"key":"16_CR18","unstructured":"Mascellani and Pedreschi. Proving termination of prolog programs. In M. Alpuente, R. Barbuti, and I. Ramos, editors, Proceedings of GULPPRODE'94, Joint conference on declarative programming, pages 46\u201361, 1994."},{"volume-title":"Types in Logic Programming","year":"1992","key":"16_CR19","unstructured":"Frank Pfenning, editor. Types in Logic Programming. MIT, Cambridge, Mass.\/London, 1992."},{"key":"16_CR20","volume-title":"Number 1407 in Lecture Notes in Mathematics","author":"W. Pohlers","year":"1989","unstructured":"Wolfram Pohlers. Proof Theory. An Introduction. Number 1407 in Lecture Notes in Mathematics. Springer-Verlag, Berlin\/Heidelberg\/New York, 1989."},{"key":"16_CR21","unstructured":"M. Presburger. \u00fcber die Vollst\u00e4ndigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt. Sprawozdanie z I Kongrescu Matematykow Krajow Slowkanskich Warszawa, pages 92\u2013101, 1929."},{"key":"16_CR22","unstructured":"Karl Stroetmann and Thomas Gla\u00df. Augmented PROLOG \u2014 An evolutionary approach. In Donald A. Smith, Olivier Ridoux, and Peter Van Roy, editors, Proceedings of the Workshop Visions for the Future of Logic Programming: Laying the Foundations for a Modern Successor to Prolog, pages 59\u201370, 1995. The Proceedings of this workshop are available at: ftp:\/\/ps-ftp.dfki.uni-sb.de\/pub\/ILPS95-FutureLP\/."},{"key":"16_CR23","unstructured":"Karl Stroetmann, Thomas Gla\u00df, and Martin M\u00fcller. Implementing safetycritical systems in Prolog: Experiences from the R&D at Siemens. In Peter Reintjes, editor, Practical Applications of Prolog '96, pages 391\u2013403, 1996."},{"key":"16_CR24","doi-asserted-by":"crossref","unstructured":"D. De Schreye, Kristof Verschaetse, and Maurice Bruynooghe. A frame-work for analysing the termination of definite logic programs with respect to call patterns. In Proceedings of the International Conference on Fifth Generation Computer Systems, pages 481\u2013488. ICOT, 1992.","DOI":"10.1007\/3-540-56282-6_5"},{"key":"16_CR25","volume-title":"Automatisierung von Terminierungsbeweisen","author":"C. Walther","year":"1990","unstructured":"Christoph Walther. Automatisierung von Terminierungsbeweisen. Vieweg, Braunschweig, Germany, 1990."},{"key":"16_CR26","first-page":"63","volume-title":"Types in Logic Programming","author":"E. Yardeni","year":"1992","unstructured":"Eyal Yardeni, Thom Fr\u00fchwirth, and Ehud Shapiro. Polymorphically typed logic programs. In Pfenning [Pfe92], pages 63\u201390."}],"container-title":["Lecture Notes in Computer Science","Static Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-61739-6_44.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:10:08Z","timestamp":1605647408000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-61739-6_44"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540617396","9783540706748"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/3-540-61739-6_44","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1996]]}}}