{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T15:53:09Z","timestamp":1725551589750},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540305538"},{"type":"electronic","value":"9783540316503"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11591191_30","type":"book-chapter","created":{"date-parts":[[2005,11,22]],"date-time":"2005-11-22T09:44:25Z","timestamp":1132652665000},"page":"427-442","source":"Crossref","is-referenced-by-count":5,"title":["Reasoning About Incompletely Defined Programs"],"prefix":"10.1007","author":[{"given":"Christoph","family":"Walther","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stephan","family":"Schweitzer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"30_CR1","unstructured":"http:\/\/www.verifun.org"},{"key":"30_CR2","unstructured":"Arthan, R.D.: Undefinedness in Z: Issues for Specification and Proof. In: Proc. CADE 13 Workshop on Mechanization of Partial Functions New Brunswick, NJ (1996), available from, \n                  \n                    http:\/\/www.cs.bham.ac.uk\/~mmk\/cade96-partiality\/"},{"key":"30_CR3","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1007\/3-540-48660-7_15","volume-title":"Automated Deduction - CADE-16","author":"S. Autexier","year":"1999","unstructured":"Autexier, S., Hutter, D., Mantel, H., Schairer, A.: inka 5.0 - A Logic Voyager. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol.\u00a01632, pp. 207\u2013211. Springer, Heidelberg (1999)"},{"key":"30_CR4","volume-title":"A Computational Logic","author":"R.S. Boyer","year":"1979","unstructured":"Boyer, R.S., Moore, J.S.: A Computational Logic. Acad. Press, NY (1979)"},{"key":"30_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"647","DOI":"10.1007\/3-540-52885-7_123","volume-title":"10th International Conference on Automated Deduction","author":"A. Bundy","year":"1990","unstructured":"Bundy, A., van Harmelen, F., Horn, C., Smaill, A.: The Oyster-Clam System. In: Stickel, M.E. (ed.) CADE 1990. LNCS, vol.\u00a0449, pp. 647\u2013648. Springer, Heidelberg (1990)"},{"key":"30_CR6","doi-asserted-by":"publisher","first-page":"913","DOI":"10.1016\/B978-044450813-3\/50016-3","volume-title":"Handb. of Autom. Reasoning","author":"H. Comon","year":"2001","unstructured":"Comon, H.: Inductionless Induction. In: Robinson, A., Voronkov, A. (eds.) Handb. of Autom. Reasoning, vol.\u00a0I, ch.14, pp. 913\u2013962. Elsevier, Amsterdam (2001)"},{"key":"30_CR7","unstructured":"Farmer, W.M.: Mechanizing the Traditional Approach to Partial Functions. In: Proc. CADE 13 Workshop on Mechanization of Partial Functions New Brunswick, NJ (1996), available from, \n                  \n                    http:\/\/www.cs.bham.ac.uk\/~mmk\/cade96-partiality\/"},{"key":"30_CR8","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1023\/A:1005702928286","volume":"18","author":"S. Finn","year":"1997","unstructured":"Finn, S., Fourmann, M.P., Longley, J.: Partial Functions in a Total Setting. Journal of Automated Reasoning\u00a018, 85\u2013104 (1997)","journal-title":"Journal of Automated Reasoning"},{"key":"30_CR9","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1023\/A:1006408829523","volume":"26","author":"J. Giesl","year":"2001","unstructured":"Giesl, J.: Induction Proofs with Partial Functions. J. Aut. Reason.\u00a026, 1\u201349 (2001)","journal-title":"J. Aut. Reason."},{"key":"30_CR10","doi-asserted-by":"crossref","first-page":"135","DOI":"10.1007\/978-94-017-0437-3_6","volume-title":"Automated Deduction - A Basis for Applications","author":"J. Giesl","year":"1998","unstructured":"Giesl, J., Walther, C., Brauburger, J.: Termination Analysis for Functional Programs. In: Bibel, W., Schmitt, P. (eds.) Automated Deduction - A Basis for Applications, vol.\u00a03, pp. 135\u2013164. Kluwer Acad. Publ., Dordrecht (1998)"},{"key":"30_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"366","DOI":"10.1007\/BFb0015254","volume-title":"Computer Science Today","author":"D. Gries","year":"1995","unstructured":"Gries, D., Schneider, F.B.: Avoiding the Undefined by Underspecification. In: van Leeuwen, J. (ed.) Computer Science Today. LNCS, vol.\u00a01000, pp. 366\u2013373. Springer, Heidelberg (1995)"},{"key":"30_CR12","doi-asserted-by":"crossref","unstructured":"Jones, C.B.: Partial functions and logics: A warning. Information Processing Letters\u00a054(2) (1995)","DOI":"10.1016\/0020-0190(95)00042-B"},{"key":"30_CR13","series-title":"Lecture Notes in Computer Science","volume-title":"Automated Deduction - Cade-13","author":"C.B. Jones","year":"1996","unstructured":"Jones, C.B.: TANSTAAFL (with partial functions). In: McRobbie, M.A., Slaney, J.K. (eds.) CADE 1996. LNCS, vol.\u00a01104. Springer, Heidelberg (1996)"},{"key":"30_CR14","first-page":"177","volume-title":"Automated Reasoning and Its Applications \u2013 Essays in Honor of Larry Wos","author":"D. Kapur","year":"1997","unstructured":"Kapur, D.: Constructors Can Be Partial, Too. In: Veroff, R. (ed.) Automated Reasoning and Its Applications \u2013 Essays in Honor of Larry Wos, pp. 177\u2013210. The MIT Press, Cambridge (1997)"},{"key":"30_CR15","first-page":"367","volume-title":"Symposium on Logic in Computer Science","author":"D. Kapur","year":"1986","unstructured":"Kapur, D., Musser, D.R.: Inductive Reasoning with Incomplete Specifications. In: Symposium on Logic in Computer Science, Cambridge, MA, vol.\u00a0720, pp. 367\u2013377. IEEE Computer Society Press, Los Alamitos (1986)"},{"issue":"2","key":"30_CR16","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1016\/0004-3702(87)90017-8","volume":"31","author":"D. Kapur","year":"1987","unstructured":"Kapur, D., Musser, D.R.: Proof by Consistency. Artificial Intelligence\u00a031(2), 125\u2013157 (1987)","journal-title":"Artificial Intelligence"},{"issue":"1-2","key":"30_CR17","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/BF00244459","volume":"16","author":"D. Kapur","year":"1996","unstructured":"Kapur, D., Subramaniam, M.: New Uses of Linear Arithmetic in Automated Theorem Proving by Induction. J. Automated Reasoning\u00a016(1-2), 39\u201378 (1996)","journal-title":"J. Automated Reasoning"},{"key":"30_CR18","unstructured":"Kaufmann, M., Moore, J.S.: ACL2: An Industrial Strength Version of NQTHM. In: Compass 1996: 11th Annual Conf. on Computer Assurance, Maryland, National Institute of Standards and Technology (1996)"},{"key":"30_CR19","volume-title":"Specification of Abstract Data Types","author":"J. Loeckx","year":"1996","unstructured":"Loeckx, J., Ehrich, H.-D., Wolf, M.: Specification of Abstract Data Types. Wiley-Teubner, New York (1996)"},{"key":"30_CR20","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1023\/B:JARS.0000009505.07087.34","volume":"31","author":"P. Manolios","year":"2003","unstructured":"Manolios, P., Moore, J.S.: Partial Functions in ACL2. Journal of Automated Reasoning\u00a031, 107\u2013127 (2003)","journal-title":"Journal of Automated Reasoning"},{"issue":"2","key":"30_CR21","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1093\/comjnl\/42.2.73","volume":"42","author":"B. Schieder","year":"1999","unstructured":"Schieder, B., Broy, M.: Adapting Calculational Logic to the Undefined. The Computer Journal\u00a042(2), 73\u201381 (1999)","journal-title":"The Computer Journal"},{"issue":"1","key":"30_CR22","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1016\/0004-3702(94)90063-9","volume":"71","author":"C. Walther","year":"1994","unstructured":"Walther, C.: On Proving the Termination of Algorithms by Machine. Artificial Intelligence\u00a071(1), 101\u2013157 (1994)","journal-title":"Artificial Intelligence"},{"key":"30_CR23","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"322","DOI":"10.1007\/978-3-540-45085-6_28","volume-title":"Automated Deduction \u2013 CADE-19","author":"C. Walther","year":"2003","unstructured":"Walther, C., Schweitzer, S.: About veriFun. In: Baader, F. (ed.) CADE 2003. LNCS (LNAI), vol.\u00a02741, pp. 322\u2013327. Springer, Heidelberg (2003)"},{"key":"30_CR24","unstructured":"Walther, C., Schweitzer, S.: Automated Termination Analysis for Incompletely Defined Programs. Technical Report VFR 04\/03, Programmiermethodik, Technische Universit\u00e4t Darmstadt (2004)"},{"key":"30_CR25","unstructured":"Walther, C., Schweitzer, S.: Reasoning about Incompletely Defined Programs. Technical Report VFR 04\/02, Programmiermethodik, Technische Universit\u00e4t Darmstadt (2004)"},{"issue":"1","key":"30_CR26","first-page":"35","volume":"32","author":"C. Walther","year":"2004","unstructured":"Walther, C., Schweitzer, S.: Verification in the Classroom. Journal of Automated Reasoning - Special Issue on Automated Reasoning and Theorem Proving in Education\u00a032(1), 35\u201373 (2004)","journal-title":"Journal of Automated Reasoning - Special Issue on Automated Reasoning and Theorem Proving in Education"},{"key":"30_CR27","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"332","DOI":"10.1007\/978-3-540-32275-7_22","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"C. Walther","year":"2005","unstructured":"Walther, C., Schweitzer, S.: Automated Termination Analysis for Incompletely Defined Programs. In: Baader, F., Voronkov, A. (eds.) LPAR 2004. LNCS (LNAI), vol.\u00a03452, pp. 332\u2013346. Springer, Heidelberg (2005)"}],"container-title":["Lecture Notes in Computer Science","Logic for Programming, Artificial Intelligence, and Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11591191_30.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T06:51:33Z","timestamp":1619506293000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11591191_30"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540305538","9783540316503"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/11591191_30","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}