{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,12,29]],"date-time":"2022-12-29T20:17:36Z","timestamp":1672345056591},"reference-count":29,"publisher":"Elsevier BV","issue":"1","license":[{"start":{"date-parts":[[2003,5,1]],"date-time":"2003-05-01T00:00:00Z","timestamp":1051747200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,29]],"date-time":"2013-07-29T00:00:00Z","timestamp":1375056000000},"content-version":"vor","delay-in-days":3742,"URL":"http:\/\/creativecommons.org\/licenses\/by-nc-nd\/3.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Electronic Notes in Theoretical Computer Science"],"published-print":{"date-parts":[[2003,5]]},"DOI":"10.1016\/s1571-0661(04)80648-0","type":"journal-article","created":{"date-parts":[[2004,9,29]],"date-time":"2004-09-29T16:47:47Z","timestamp":1096476467000},"page":"1-8","source":"Crossref","is-referenced-by-count":2,"title":["Deduction as an Engineering Science"],"prefix":"10.1016","volume":"86","author":[{"given":"Dieter","family":"Hutter","sequence":"first","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/S1571-0661(04)80648-0_NEWBIB1","doi-asserted-by":"crossref","unstructured":"S. Autexier, D. Hutter, T. Mossakowski and A. Schairer. The development graph manager MAYA. In Proceedings 9th International Conference on Algebraic Methodology And Software Technology, AMAST2002. Springer-Verlag, LNCS, (2002)","DOI":"10.1007\/3-540-45719-4_34"},{"key":"10.1016\/S1571-0661(04)80648-0_NEWBIB2","series-title":"A Computational Logic","author":"Boyer","year":"1979"},{"key":"10.1016\/S1571-0661(04)80648-0_NEWBIB3","first-page":"83","article-title":"Integrating Decision Procedures into Heuristic Theorem Provers: A Case Study of Linear Arithmetic","author":"Boyer","year":"1988"},{"key":"10.1016\/S1571-0661(04)80648-0_NEWBIB4","series-title":"\u201cRippling: Meta-level Guidance for Mathematical Reasoning\u201d","author":"Bundy","year":"2003"},{"key":"10.1016\/S1571-0661(04)80648-0_NEWBIB5","doi-asserted-by":"crossref","unstructured":"W.M. Farmer. An Infrastructure for Intertheory Reasoning. 17th International Conference on Automated Deduction CADE-17, (2000)","DOI":"10.1007\/10721959_8"},{"key":"10.1016\/S1571-0661(04)80648-0_NEWBIB6","doi-asserted-by":"crossref","unstructured":"W.M. Farmer, J.D. Guttman and F. J. Thayer. IMPS: An Interactive Mathematical Proof System. 10thInternational Conference on Automated Deduction CADE-10, 1990","DOI":"10.1007\/3-540-52885-7_126"},{"key":"10.1016\/S1571-0661(04)80648-0_NEWBIB7","doi-asserted-by":"crossref","unstructured":"A. Felty, D. Howe: Generalization and Reuse of Tactic Proofs. In: 5th International Conference on Logic Programming and Automated Reasoning, LPAR-94, Springer-Verlag, LNAI 822, 1994","DOI":"10.1007\/3-540-58216-9_25"},{"issue":"3","key":"10.1016\/S1571-0661(04)80648-0_NEWBIB8","first-page":"156","article-title":"Agent-Oriented Integration of Distributed Mathematical Services","volume":"5","author":"Franke","year":"1999","journal-title":"Journal of Universal Computer Science"},{"key":"10.1016\/S1571-0661(04)80648-0_NEWBIB9","unstructured":"F. Giunchiglia, P. Pecchiari and C. Talcott. Reasoning Theories - Towards an Architecture for Open Mechanized Reasoning Systems In F. Baader and K. U. Schulz (eds): Frontiers of Combining Systems: Proceedings of the 1st International Workshop, Munich (Germany), Kluwer Academic Publishers, 157\u2013174, (1996)"},{"issue":"3\u20134","key":"10.1016\/S1571-0661(04)80648-0_NEWBIB10","first-page":"167","article-title":"Theories of Abstraction","volume":"10","author":"Giunchiglia","year":"1997","journal-title":"AI Communications"},{"issue":"2\u20133","key":"10.1016\/S1571-0661(04)80648-0_NEWBIB11","doi-asserted-by":"crossref","first-page":"323","DOI":"10.1016\/0004-3702(92)90021-O","article-title":"A theory of abstraction","volume":"57","author":"Giunchiglia","year":"1992","journal-title":"Artificial Intelligence"},{"key":"10.1016\/S1571-0661(04)80648-0_NEWBIB12","series-title":"Principles of Programming Languages, POPL 2002","article-title":"Lazy Abstraction","author":"Henzinger","year":"2002"},{"key":"10.1016\/S1571-0661(04)80648-0_NEWBIB13","unstructured":"J.R. Hobbs. Granularity. In Arivind Joshi, editor, Proceedings of the Ninth International Joint Conference on Artificial Intelligence, pages 1\u20134, Los Altos, California, 1985. Morgan Kaufmann."},{"key":"10.1016\/S1571-0661(04)80648-0_NEWBIB14","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1023\/A:1018980012242","article-title":"Annotated reasoning","volume":"29","author":"Hutter","year":"2000","journal-title":"Annals of Mathematics and Artificial Intelligence (AMAI). Special Issue on Strategies in Automated Deduction"},{"issue":"4","key":"10.1016\/S1571-0661(04)80648-0_NEWBIB15","doi-asserted-by":"crossref","DOI":"10.1080\/095281300454784","article-title":"Formal software development in the verification support environment","volume":"12","author":"Hutter","year":"2000","journal-title":"Journal of Experimental and Theoretical Artificial Intelligence"},{"key":"10.1016\/S1571-0661(04)80648-0_NEWBIB16","doi-asserted-by":"crossref","unstructured":"D. Hutter and A. Schairer. Towards an evolutionary formal software development. In Proceedings 16th IEEE International Conference on Automated Software Engineering, ASE-2001, San Diego, USA, IEEE Computer Society, (2001)","DOI":"10.1109\/ASE.2001.989842"},{"key":"10.1016\/S1571-0661(04)80648-0_NEWBIB17","series-title":"Mechanizing Mathematical Reasoning, Techniques, Tools, and Applications, Festschrift in honour of J\u00f6rg H. Siekmann","year":"2003"},{"issue":"1\u20132","key":"10.1016\/S1571-0661(04)80648-0_NEWBIB18","doi-asserted-by":"crossref","first-page":"79","DOI":"10.1007\/BF00244460","article-title":"Productive Use of failure in inductive proof","volume":"16","author":"Ireland","year":"1996","journal-title":"Journal of Automated Reasoning"},{"key":"10.1016\/S1571-0661(04)80648-0_NEWBIB19","doi-asserted-by":"crossref","unstructured":"M. Kerber and M. Kohlhase (eds) Symbolic Computation and Automated Reasoning - The Calculemus-2000 Symposium, A K Peters Publishers, USA, (2000)","DOI":"10.1201\/9781439864234"},{"key":"10.1016\/S1571-0661(04)80648-0_NEWBIB20","doi-asserted-by":"crossref","first-page":"147","DOI":"10.1016\/0004-3702(71)90008-7","article-title":"A paradigm for reasoning by analogy","volume":"2","author":"Kling","year":"1971","journal-title":"Artificial Intelligence"},{"issue":"1\u20132","key":"10.1016\/S1571-0661(04)80648-0_NEWBIB21","first-page":"17","article-title":"Proving Theorems by Reuse","volume":"116","author":"Kolbe","year":"2000","journal-title":"Artificial Intelligence"},{"key":"10.1016\/S1571-0661(04)80648-0_NEWBIB22","series-title":"Computer Aided Verification of Coordinating Processes","author":"Kurshan","year":"1994"},{"issue":"1","key":"10.1016\/S1571-0661(04)80648-0_NEWBIB23","article-title":"Automated Deduction: Looking ahead","volume":"20","author":"Loveland","year":"1999","journal-title":"AI-Magazine"},{"issue":"3","key":"10.1016\/S1571-0661(04)80648-0_NEWBIB24","doi-asserted-by":"crossref","first-page":"263","DOI":"10.1023\/A:1005843212881","article-title":"Solution of the Robbins Problem","volume":"19","author":"McCune","year":"1997","journal-title":"Journal of Automated Reasoning"},{"key":"10.1016\/S1571-0661(04)80648-0_NEWBIB25","unstructured":"T.F. Melham. Formalizing Abstraction Mechanisms for Hardware Verification in Higher Order Logic. PhD thesis, Computer Laboratory, University of Cambridge, 1990."},{"key":"10.1016\/S1571-0661(04)80648-0_NEWBIB26","unstructured":"E. Melis: A model of analogy-driven proof-plan construction. In 14th International Joint Conference on Artificial Intelligence, Morgan Kaufman Publ. pages 182\u2013189, Montreal, 1995."},{"key":"10.1016\/S1571-0661(04)80648-0_NEWBIB27","unstructured":"S. Owre, S. Rajan, J.M. Rushby, N. Shankar and M. K. Srivas PVS: Combining specification, proof checking, and model checking, Proceedings of the 18th International Conference on Computer Aided Verification CAV, Springer, LNCS 1102, New Brunswick, NJ, USA, (1996)"},{"key":"10.1016\/S1571-0661(04)80648-0_NEWBIB28","doi-asserted-by":"crossref","unstructured":"D. Plaisted. Abstraction mappings in mechanical theorem proving. In Proceedings of the Fifth International Conference on Automated Deduction, volume 87 of Lecture Notes in Computer Science, pages 264\u2013280, Les Arcs, France, 1980. Springer-Verlag.","DOI":"10.1007\/3-540-10009-1_21"},{"key":"10.1016\/S1571-0661(04)80648-0_NEWBIB29","doi-asserted-by":"crossref","unstructured":"A. Voronkov. Algorithms, Datastructures, and Other Issues in Efficient Automated Deduction, Proceedings of the 1st International Joint Conference on Automated Reasoning, IJACR 2001, Springer, LNAI 2083, (2001)","DOI":"10.1007\/3-540-45744-5_3"}],"container-title":["Electronic Notes in Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066104806480?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066104806480?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2020,4,3]],"date-time":"2020-04-03T07:14:23Z","timestamp":1585898063000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S1571066104806480"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003,5]]},"references-count":29,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2003,5]]}},"alternative-id":["S1571066104806480"],"URL":"https:\/\/doi.org\/10.1016\/s1571-0661(04)80648-0","relation":{},"ISSN":["1571-0661"],"issn-type":[{"value":"1571-0661","type":"print"}],"subject":[],"published":{"date-parts":[[2003,5]]}}}