{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,19]],"date-time":"2025-05-19T04:01:18Z","timestamp":1747627278787,"version":"3.40.5"},"reference-count":24,"publisher":"Springer Science and Business Media LLC","issue":"3-4","license":[{"start":{"date-parts":[[1998,7,1]],"date-time":"1998-07-01T00:00:00Z","timestamp":899251200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[1998,7,1]],"date-time":"1998-07-01T00:00:00Z","timestamp":899251200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Annals of Mathematics and Artificial Intelligence"],"published-print":{"date-parts":[[1998,7]]},"DOI":"10.1023\/a:1018943603394","type":"journal-article","created":{"date-parts":[[2003,2,19]],"date-time":"2003-02-19T22:07:13Z","timestamp":1045692433000},"page":"259-279","source":"Crossref","is-referenced-by-count":1,"title":["Automating the synthesis of decision procedures in a constructive metatheory"],"prefix":"10.1007","volume":"22","author":[{"given":"Alessandro","family":"Armando","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jason","family":"Gallagher","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alan","family":"Smaill","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alan","family":"Bundy","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"325483_CR1","series-title":"Lecture Notes in Artificial Intelligence","volume-title":"Proc. 3rd Conf. of the Italian Association for Artificial Intelligence","author":"A. Armando","year":"1993","unstructured":"A. Armando, A. Cimatti and L. Vigan\u00f2, Building and executing proof strategies in a formal metatheory, in: Proc. 3rd Conf. of the Italian Association for Artificial Intelligence, Lecture Notes in Artificial Intelligence, Vol. 728 (Springer, Berlin, 1993)."},{"key":"325483_CR2","volume-title":"Logical Environments","author":"D. Basin","year":"1993","unstructured":"D. Basin and R. Constable, Metalogical frameworks, in: Logical Environments, eds. G. Huet and G. Plotkin (Cambridge University Press, Cambridge, 1993)."},{"key":"325483_CR3","unstructured":"S. Biundo, A synthesis system mechanizing proofs by induction, in: Proc. 1986 European Conf. on Artificial Intelligence(1986) pp. 69-78."},{"key":"325483_CR4","unstructured":"S. Biundo, Automated synthesis of recursive algorithms as a theorem proving tool, in: Proc. 8th European Conference on Artificial Intelligence, ed. Y. Kodratoff (Pitman, 1988) pp. 553-558."},{"issue":"2","key":"325483_CR5","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1007\/BF00881856","volume":"14","author":"A. Bouhoula","year":"1995","unstructured":"A. Bouhoula and M. Rusinowitch, Implicit induction in conditional theories, Journal of Automated Reasoning 14(2) (1995) 189-235.","journal-title":"Journal of Automated Reasoning"},{"key":"325483_CR6","volume-title":"A Computational Logic","author":"R.S. Boyer","year":"1979","unstructured":"R.S. Boyer and J.S. Moore, A Computational Logic(Academic Press, New York, 1979)."},{"key":"325483_CR7","first-page":"103","volume-title":"The Correctness Problem in Computer Science","author":"R.S. Boyer","year":"1981","unstructured":"R.S. Boyer and J.S. Moore, Metafunctions, in: The Correctness Problem in Computer Science, eds. R.S. Boyer and J.S. Moore (Academic Press, New York, 1981) pp. 103-184."},{"key":"325483_CR8","volume-title":"Perspectives in Computing","author":"R.S. Boyer","year":"1988","unstructured":"R.S. Boyer and J.S. Moore, A Computational Logic Handbook, Perspectives in Computing, Vol. 23 (Academic Press, New York, 1988)."},{"key":"325483_CR9","series-title":"Longer version available from Edinburgh as DAI Research Paper","doi-asserted-by":"crossref","first-page":"111","DOI":"10.1007\/BFb0012826","volume-title":"Proc. 9th Conf. on Automated Deduction","author":"A. Bundy","year":"1988","unstructured":"A. Bundy, The use of explicit plans to guide inductive proofs, in: Proc. 9th Conf. on Automated Deduction, eds. R. Lusk and R. Overbeek (Springer, Berlin, 1988) pp. 111-120. Longer version available from Edinburgh as DAI Research Paper No. 349."},{"key":"325483_CR10","unstructured":"A. Bundy, ed., Proc. 12th Conf. on Automated Deduction, Nancy, France, Lecture Notes in Artificial Intelligence, Vol. 814 (Springer, Berlin, 1994)."},{"key":"325483_CR11","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 (1993) 185-253.","journal-title":"Artificial Intelligence"},{"key":"325483_CR12","doi-asserted-by":"publisher","first-page":"303","DOI":"10.1007\/BF00249016","volume":"7","author":"A. Bundy","year":"1991","unstructured":"A. Bundy, F. van Harmelen, J. Hesketh and A. Smaill, Experiments with proof plans for induction, Journal of Automated Reasoning 7 (1991) 303-324.","journal-title":"Journal of Automated Reasoning"},{"key":"325483_CR13","unstructured":"A. Bundy, F. van Harmelen, J. Hesketh, A. Smaill and A. Stevens, A rational reconstruction and extension of recursion analysis, in: Proceedings of the Eleventh International Joint Conference on Artificial Intelligence, ed. N.S. Sridharan (Morgan Kaufmann, 1989) pp. 359-365."},{"key":"325483_CR14","volume-title":"Implementing Mathematics with the Nuprl Proof Development System","author":"R.L. Constable","year":"1986","unstructured":"R.L. Constable, S.F. Allen, H.M. Bromley et al., Implementing Mathematics with the Nuprl Proof Development System(Prentice-Hall, Englewood Cliffs, NJ, 1986)."},{"key":"325483_CR15","first-page":"45","volume-title":"Formal Techniques in Artificial Intelligence: A Sourcebook","author":"R.L. Constable","year":"1990","unstructured":"R.L. Constable and D.J. Howe, Implementing metamathematics as an approach to automatic theorem proving, in: Formal Techniques in Artificial Intelligence: A Sourcebook, ed. R.B. Banerji (North-Holland, Amsterdam, 1990) pp. 45-76."},{"key":"325483_CR16","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1145\/321033.321034","volume":"7","author":"M. Davis","year":"1960","unstructured":"M. Davis and H. Putnam, A computing procedure for quantification theory, Journal of the Association for Computing Machinery 7 (1960) 201-215.","journal-title":"Journal of the Association for Computing Machinery"},{"issue":"3","key":"325483_CR17","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1016\/0304-3975(82)90026-3","volume":"17","author":"N. Dershowitz","year":"1982","unstructured":"N. Dershowitz, Orderings for term-rewriting systems, Theoretical Computer Science 17(3) (March 1982) 279-301.","journal-title":"Theoretical Computer Science"},{"key":"325483_CR18","doi-asserted-by":"publisher","first-page":"795","DOI":"10.2307\/2275431","volume":"57","author":"R. Dyckhoff","year":"1992","unstructured":"R. Dyckhoff, Contraction-free sequent calculi for intuitionistic logic, Journal of Symbolic Logic 57 (1992) 795-807.","journal-title":"Journal of Symbolic Logic"},{"key":"325483_CR19","first-page":"191","volume-title":"Logic Colloquium' 88","author":"S. Feferman","year":"1989","unstructured":"S. Feferman, Finitary inductively presented logics, in: Logic Colloquium' 88(North-Holland, Amsterdam, 1989) pp. 191-220."},{"key":"325483_CR20","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1016\/0004-3702(95)00002-X","volume":"80","author":"F. Giunchiglia","year":"1996","unstructured":"F. Giunchiglia and P. Traverso, A metatheory of a mechanized object theory, Artificial Intelligence 80 (1996) 197-241.","journal-title":"Artificial Intelligence"},{"issue":"1","key":"325483_CR21","doi-asserted-by":"publisher","first-page":"90","DOI":"10.1145\/357084.357090","volume":"2","author":"Z. Manna","year":"1980","unstructured":"Z. Manna and R.J. Waldinger, A deductive approach to program synthesis, ACM Transactions on Programming Languages and Systems 2(1) (1980) 90-121.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"325483_CR22","first-page":"61","volume-title":"Logical Environments","author":"S. Matthews","year":"1993","unstructured":"S. Matthews, A. Smaill and D. Basin, Experience with FS0 as a framework theory, in: Logical Environments, eds. G. Huet and G. Plotkin (Cambridge University Press, Cambridge, 1993) pp. 61- 82."},{"key":"325483_CR23","doi-asserted-by":"crossref","first-page":"415","DOI":"10.1093\/oso\/9780198537618.003.0004","volume-title":"Handbook of Logic in Computer Science","author":"L.C. Paulson","year":"1992","unstructured":"L.C. Paulson, Designing a theorem prover, in: Handbook of Logic in Computer Science, eds. S. Abramsky, D.M. Gabbay and T.S.E. Maibaum, Vol. 2 (Oxford University Press, Oxford, 1992) pp. 415-475."},{"key":"325483_CR24","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"341","DOI":"10.1007\/3-540-58156-1_24","volume-title":"Proc. 12th Conf. on Automated Deduction, Nancy, France","author":"M. Stickel","year":"1994","unstructured":"M. Stickel, R. Waldinger, M. Lowry, T. Pressburger and I. Underwood, Deductive composition of astronomical software from subroutine libraries, in: Proc. 12th Conf. on Automated Deduction, Nancy, France, Lecture Notes in Artificial Intelligence, Vol. 814, ed. A. Bundy (Springer, Berlin, 1994) pp. 341-355."}],"container-title":["Annals of Mathematics and Artificial Intelligence"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1018943603394.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1018943603394\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1018943603394.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,18]],"date-time":"2025-05-18T05:48:44Z","timestamp":1747547324000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1018943603394"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998,7]]},"references-count":24,"journal-issue":{"issue":"3-4","published-print":{"date-parts":[[1998,7]]}},"alternative-id":["325483"],"URL":"https:\/\/doi.org\/10.1023\/a:1018943603394","relation":{},"ISSN":["1012-2443","1573-7470"],"issn-type":[{"type":"print","value":"1012-2443"},{"type":"electronic","value":"1573-7470"}],"subject":[],"published":{"date-parts":[[1998,7]]}}}