{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T21:11:30Z","timestamp":1725484290208},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540440390"},{"type":"electronic","value":"9783540456858"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45685-6_13","type":"book-chapter","created":{"date-parts":[[2007,5,19]],"date-time":"2007-05-19T20:47:53Z","timestamp":1179607673000},"page":"182-197","source":"Crossref","is-referenced-by-count":0,"title":["A Comparison of Two Proof Critics: Power vs. Robustness"],"prefix":"10.1007","author":[{"given":"Louise A.","family":"Dennis","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alan","family":"Bundy","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,7,25]]},"reference":[{"issue":"1\u20132","key":"13_CR1","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/BF00244462","volume":"16","author":"D. Basin","year":"1996","unstructured":"D. Basin and T. Walsh. A calculus for and termination of rippling. Journal of Automated Reasoning, 16(1\u20132):147\u2013180, 1996.","journal-title":"Journal of Automated Reasoning"},{"key":"13_CR2","doi-asserted-by":"crossref","unstructured":"A. Bundy. The use of explicit plans to guide inductive proofs. In R. Lusk and R. Overbeek, editors, 9th Conference on Automated Deduction, pages 111\u2013120. Springer-Verlag, 1988. Longer version available from Edinburgh as DAI Research Paper No. 349.","DOI":"10.1007\/BFb0012826"},{"key":"13_CR3","doi-asserted-by":"crossref","unstructured":"A. Bundy. The automation of proof by mathematical induction. In A Robinson and A. Voronkov, editors, Handbook of Automated Reasoning, Volume 1. Elsevier, 2001.","DOI":"10.1016\/B978-044450813-3\/50015-1"},{"key":"13_CR4","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1016\/0004-3702(93)90079-Q","volume":"62","author":"A. Bundy","year":"1993","unstructured":"A. Bundy, A. Stevens, F. van Harmelen, A. Ireland, and A. Smaill. Rippling: A heuristic for guiding inductive proofs. Artificial Intelligence, 62:185\u2013253, 1993. Also available from Edinburgh as DAI Research Paper No. 567.","journal-title":"Artificial Intelligence"},{"key":"13_CR5","doi-asserted-by":"crossref","unstructured":"A. Bundy, F. van Harmelen, C. Horn, and A. Smaill. The Oyster-Clam system. In M.E. Stickel, editor, 10th International Conference on Automated Deduction, pages 647\u2013648. Springer-Verlag, 1990. Lecture Notes in Artificial Intelligence No. 449. Also available from Edinburgh as DAI Research Paper 507.","DOI":"10.1007\/3-540-52885-7_123"},{"key":"13_CR6","unstructured":"C. Castellini and A. Smaill. Tactic-based theorem proving in first-order modal and temporal logics. In IJCAR 2001, workshop t10, 2001."},{"key":"13_CR7","series-title":"Lect Notes Comput Sci","volume-title":"KI 2001: Advances in Artificial Intelligence, Joint German\/Austrian Conference on AI, Vienna, Austria, September 19\u201321, 2001, Proceedings","author":"A. Degtyarev","year":"2001","unstructured":"A. Degtyarev and M. Fisher. Towards first-order temporal resolution. In F. Baader, G. Brewka, and T. Eiter, editors, KI 2001: Advances in Artificial Intelligence, Joint German\/Austrian Conference on AI, Vienna, Austria, September 19\u201321, 2001, Proceedings, volume 2174 of Lecture Notes in Computer Science. Springer, 2001."},{"key":"13_CR8","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1023\/A:1018940332714","volume":"29","author":"L. A. Dennis","year":"2000","unstructured":"L. A. Dennis, A. Bundy, and I. Green. Making a productive use of failure to generate witness for coinduction from divergent proof attempts. Annals of Mathematics and Artificial Intelligence, 29:99\u2013138, 2000. Also available from Edinburgh as Informatics Report RR0004.","journal-title":"Annals of Mathematics and Artificial Intelligence"},{"key":"13_CR9","doi-asserted-by":"crossref","unstructured":"M. Fisher, C. Dixon, and M. Peim. Clausal temporal resolution. ACM Transactions on Computational Logic, 1(4), 2001.","DOI":"10.1145\/371282.371311"},{"key":"13_CR10","doi-asserted-by":"crossref","unstructured":"D.M. Gabbay, I. Hodkinson, and M. Reynolds. Temporal Logic: Mathematical Foundations and Computational Aspects. Oxford University Press, 1994.","DOI":"10.1007\/BFb0013976"},{"key":"13_CR11","first-page":"79","volume-title":"Journal of Automated Reasoning","author":"A. Ireland","year":"1996","unstructured":"A. Ireland and A. Bundy. Productive use of failure in inductive proof. Journal of Automated Reasoning, 16(1\u20132):79\u2013111, 1996. Also available as DAI Research Paper No 716, Dept. of Artificial Intelligence, Edinburgh."},{"key":"13_CR12","unstructured":"C. B. Jones. Software Development: A Rigorous Approach. Prentice-Hall international series in Computer Science. Prentice-Hall, 1980."},{"key":"13_CR13","unstructured":"J. Richardson and A. Smaill. Continuations of proof strategies. In M.P. Bonacina and B. Gramlich, editors, Proc. 4th International Workshop on Strategies in Automated Deduction (STRATEGIES 2001), Siena, Italy, june 2001. Available from \n                    http:\/\/www.logic.at\/strategies\/strategies01\/\n                    \n                  ."},{"key":"13_CR14","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1007\/BFb0054254","volume-title":"Conference on Automated Deduction (CADE\u201998)","author":"J.D.C. Richardson","year":"1998","unstructured":"J.D.C. Richardson, A. Smaill, and I. Green. System description: Proof planning in higher-order logic with lambda-clam. In C. Kirchner and H. Kirchner, editors, Conference on Automated Deduction (CADE\u201998), volume 1421 of Lecture Notes in Computer Science, pages 129\u2013133. Springer-Verlag, 1998."},{"key":"13_CR15","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"399","DOI":"10.1007\/BFb0105418","volume-title":"Theorem Proving in Higher Order Logics: 9th International Conference, TPHOLs\u201996","author":"A. Smaill","year":"1996","unstructured":"A. Smaill and I. Green. Higher-order annotated terms for proof search. In J. von Wright, J. Grundy, and J. Harrison, editors, Theorem Proving in Higher Order Logics: 9th International Conference, TPHOLs\u201996, volume 1275 of Lecture Notes in Computer Science, pages 399\u2013414, Turku, Finland, 1996. Springer-Verlag. Also available from Edinburgh as DAI Research Paper 799."},{"key":"13_CR16","doi-asserted-by":"crossref","first-page":"209","DOI":"10.1613\/jair.275","volume":"4","author":"T. Walsh","year":"1996","unstructured":"T. Walsh. A divergence critic for inductive proof. Journal of Artificial Intelligence Research, 4:209\u2013235, 1996.","journal-title":"Journal of Artificial Intelligence Research"}],"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\/3-540-45685-6_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,2,16]],"date-time":"2019-02-16T19:42:09Z","timestamp":1550346129000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45685-6_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540440390","9783540456858"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/3-540-45685-6_13","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}