{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:12:53Z","timestamp":1761610373777,"version":"build-2065373602"},"reference-count":17,"publisher":"Elsevier BV","issue":"3","license":[{"start":{"date-parts":[[1999,1,1]],"date-time":"1999-01-01T00:00:00Z","timestamp":915148800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[1999,1,1]],"date-time":"1999-01-01T00:00:00Z","timestamp":915148800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/legal\/tdmrep-license"},{"start":{"date-parts":[[2013,7,29]],"date-time":"2013-07-29T00:00:00Z","timestamp":1375056000000},"content-version":"vor","delay-in-days":5323,"URL":"http:\/\/creativecommons.org\/licenses\/by-nc-nd\/3.0\/"}],"content-domain":{"domain":["elsevier.com","sciencedirect.com"],"crossmark-restriction":true},"short-container-title":["Electronic Notes in Theoretical Computer Science"],"published-print":{"date-parts":[[1999]]},"DOI":"10.1016\/s1571-0661(05)80606-1","type":"journal-article","created":{"date-parts":[[2005,5,6]],"date-time":"2005-05-06T15:34:43Z","timestamp":1115393683000},"page":"322-339","update-policy":"https:\/\/doi.org\/10.1016\/elsevier_cm_policy","source":"Crossref","is-referenced-by-count":0,"title":["The Control Component of Open Mechanized Reasoning Systems"],"prefix":"10.1016","volume":"23","author":[{"given":"Alessandro","family":"Armando","sequence":"first","affiliation":[]},{"given":"Alessandro","family":"Coglio","sequence":"additional","affiliation":[]},{"given":"Fausto","family":"Giunchiglia","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/S1571-0661(05)80606-1_BIB1","first-page":"150","article-title":"Theorems and Algorithms: An Interface between Isabelle and Maple.","author":"Ballarin","year":"1995","journal-title":"In A.H.M. Levelt, editor, Proceedings of International Symposium on Symbolic and Algebraic Computation (ISSAC\u203395)"},{"key":"10.1016\/S1571-0661(05)80606-1_BIB2","series-title":"Proceedings of the International Conference on Artificial Intelligence and Symbolic Computation (AISC\ue4f898), volume 1476 of LNAI","first-page":"94","article-title":"Specification and integration of theorem provers and computer algebra systems","author":"Bertoli","year":"1998"},{"key":"10.1016\/S1571-0661(05)80606-1_BIB3","unstructured":"P.G. Bertoli. Using OMRS in practice: a case study with ACL2. PhD thesis, Computer Science Dept., University Rome 3, Rome, 1997."},{"year":"1979","series-title":"A Computational Logic","author":"Boyer","key":"10.1016\/S1571-0661(05)80606-1_BIB4"},{"key":"10.1016\/S1571-0661(05)80606-1_BIB5","series-title":"ISSAC \u203397. Proceedings of the 1997 International Symposium on Symbolic and Algebraic Computation, July 21\u201423, 1997, Maui, Hawaii","first-page":"384","article-title":"A survey of the theorema project","author":"Buchberger","year":"1997"},{"key":"10.1016\/S1571-0661(05)80606-1_BIB6","first-page":"761","article-title":"Analytica\u2014A Theorem Prover in Mathematica","author":"Clarke","year":"1992","journal-title":"Proc. of the 11th Conference on Automated Deduction"},{"year":"1998","series-title":"Composing and Controlling Search in Reasoning Theories using Mappings., Technical report","author":"Coglio","key":"10.1016\/S1571-0661(05)80606-1_BIB7"},{"year":"1986","series-title":"Implementing Mathematics with the NuPRL Proof Development System","author":"Constable","key":"10.1016\/S1571-0661(05)80606-1_BIB8"},{"key":"10.1016\/S1571-0661(05)80606-1_BIB9","unstructured":"F. Giunchiglia, P. Pecchiari, and C. Talcott. Reasoning Theories: Towards an Architecture for Open Mechanized Reasoning Systems. Technical Report 9409-15, IRST, Trento, Italy, 1994. Also published as Stanford Computer Science Department Technical note number STAN-CS-TN-94-15, Stanford University. Short version published in Proc. of the First International Workshop on Frontiers of Combining Systems (FroCoS\u203396), Munich, Germany, March 1996."},{"key":"10.1016\/S1571-0661(05)80606-1_BIB10","doi-asserted-by":"crossref","first-page":"217","DOI":"10.1016\/0304-3975(92)90302-V","article-title":"Order-Sorted Algebra I: Equational Deduction for Multiple Inheritance, Overloading, Exceptions and Partial Operations","volume":"105","author":"Goguen","year":"1992","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/S1571-0661(05)80606-1_BIB11","series-title":"volume 78 of Lecture Notes in Computer Science.","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-09724-4","article-title":"Edinburgh LCF - A mechanized logic of computation","author":"Gordon","year":"1979"},{"year":"1998","series-title":"Theorem Proving with the Real Numbers","author":"Harrison","key":"10.1016\/S1571-0661(05)80606-1_BIB12"},{"key":"10.1016\/S1571-0661(05)80606-1_BIB13","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1023\/A:1006023127567","article-title":"A Skeptic's Approach to Combining Hol and Maple","volume":"21","author":"Harrison","year":"1998","journal-title":"Journal of Automated Reasoning"},{"key":"10.1016\/S1571-0661(05)80606-1_BIB14","doi-asserted-by":"crossref","first-page":"590","DOI":"10.1007\/3-540-58156-1_43","article-title":"Exploring Abstract Algebra in Constructive Type Theory","author":"Jackson","year":"1994","journal-title":"Proc. of the 12th Conference on Automated Deduction"},{"key":"10.1016\/S1571-0661(05)80606-1_BIB15","unstructured":"M. Kaufmann, J S. Moore., ACL2 Version 1.8 User's Manual. Available on line at http:\/\/www.cs.utexas.edu\/users\/moore\/acl2\/index.html."},{"key":"10.1016\/S1571-0661(05)80606-1_BIB16","doi-asserted-by":"crossref","first-page":"869","DOI":"10.1073\/pnas.50.5.869","article-title":"Functorial semantics of algebraic theories","volume":"50","author":"William Lawvere","year":"1963","journal-title":"Proceedings, National Academy of Sciences"},{"key":"10.1016\/S1571-0661(05)80606-1_BIB17","doi-asserted-by":"crossref","first-page":"363","DOI":"10.1007\/BF00248324","article-title":"The Foundation of a Generic Theorem Prover","volume":"5","author":"Paulson","year":"1989","journal-title":"Journal of Automated Reasoning"}],"container-title":["Electronic Notes in Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066105806061?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066105806061?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:08:21Z","timestamp":1761610101000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S1571066105806061"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"references-count":17,"journal-issue":{"issue":"3","published-print":{"date-parts":[[1999]]}},"alternative-id":["S1571066105806061"],"URL":"https:\/\/doi.org\/10.1016\/s1571-0661(05)80606-1","relation":{},"ISSN":["1571-0661"],"issn-type":[{"type":"print","value":"1571-0661"}],"subject":[],"published":{"date-parts":[[1999]]},"assertion":[{"value":"Elsevier","name":"publisher","label":"This article is maintained by"},{"value":"The Control Component of Open Mechanized Reasoning Systems","name":"articletitle","label":"Article Title"},{"value":"Electronic Notes in Theoretical Computer Science","name":"journaltitle","label":"Journal Title"},{"value":"https:\/\/doi.org\/10.1016\/S1571-0661(05)80606-1","name":"articlelink","label":"CrossRef DOI link to publisher maintained version"},{"value":"converted-article","name":"content_type","label":"Content Type"},{"value":"Copyright \u00a9 1999 Elsevier B.V.","name":"copyright","label":"Copyright"}]}}