{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:26:25Z","timestamp":1761611185573},"publisher-location":"Berlin, Heidelberg","reference-count":12,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540649601"},{"type":"electronic","value":"9783540498162"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/bfb0055905","type":"book-chapter","created":{"date-parts":[[2006,7,27]],"date-time":"2006-07-27T17:17:34Z","timestamp":1154020654000},"page":"94-106","source":"Crossref","is-referenced-by-count":10,"title":["Specification and integration of theorem provers and computer algebra systems"],"prefix":"10.1007","author":[{"given":"P. G.","family":"Bertoli","sequence":"first","affiliation":[]},{"given":"J.","family":"Calmet","sequence":"additional","affiliation":[]},{"given":"F.","family":"Giunchiglia","sequence":"additional","affiliation":[]},{"given":"K.","family":"Homann","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2006,5,27]]},"reference":[{"key":"8_CR1","unstructured":"Abbott, J. PossoXDR specifications. Internal Posso technical report, 1994."},{"key":"8_CR2","doi-asserted-by":"crossref","unstructured":"Armando, A., and Ranise, S. From Integrated Reasoning Specialists to \u201cPlug-and-Play\u2253 Reasoning Components. In Proceedings of AISC\u201998, Springer Verlag.","DOI":"10.1007\/BFb0055901"},{"key":"8_CR3","volume-title":"PhD thesis","author":"P. Bertoli","year":"1997","unstructured":"Bertoli, P.Using OMRS for real: a case study withAcl2. PhD thesis, Computer Science Dept., University Rome 3, Rome, 1997. Forthcoming."},{"key":"8_CR4","unstructured":"C. Ballarin, K. Homann, J. C. Theorems and Algorithms: An interface between Isabelle and Maple. In International Symposium on Symbolic and Agebraic Computation, ISSAC \u201995 (1995), H. M. Levelt, Ed., ACM Press, pp. 150\u2013157."},{"key":"8_CR5","doi-asserted-by":"crossref","unstructured":"Calmet, J., and Homann, K. Structures for symbolic mathematical reasoning and computation. In Proceedings of DISCO \u201996 \u2014 Design and Implementation of Symbolic Computation Systems (1996), J. Calmet and C. Limongelli, Eds.","DOI":"10.1007\/3-540-61697-7"},{"key":"8_CR6","volume-title":"Master\u2019s thesis","author":"A. Coglio","year":"1996","unstructured":"Coglio, A. Definizione di un formalismo per la specifica delle strategie di inferenza dei sistemi di ragionamento meccanizzato e sua applicazione ad un sistema allo stato dell\u2019arte. Master\u2019s thesis, University of Genoa, Italy, 1996."},{"key":"8_CR7","doi-asserted-by":"crossref","unstructured":"E. Clarke, X. Z. Analytica \u2014 a theorem prover in mathematica. In Proc. of the 10th Conference on Automated Deduction (1992), Springer-Verlag, pp. 761\u2013765.","DOI":"10.1007\/3-540-55602-8_220"},{"key":"8_CR8","volume-title":"Tech. Rep. 9409-15","author":"F. Giunchiglia","year":"1994","unstructured":"Giunchiglia, F., Pecchiari, P., and Talcott, C. Reasoning Theories: Towards an Architecture for Open Mechanized Reasoning Systems. Tech. Rep. 9409-15, IRST, Trento, Italy, 1994. Short version in Proc. of the First International Workshop on Frontiers of Combining Systems (FroCoS\u201996), Munich, Germany, 1996."},{"key":"8_CR9","doi-asserted-by":"crossref","unstructured":"J. Harrison, L. T. Extending the HOL prover with a Computer Algebra System to reason about the Reals. In Higher Order Logic Theorem proving and its Applications, J. J. Joyce and J. H. Seger, Eds. Springer-Verlag, 1993, pp. 174\u2013184.","DOI":"10.1007\/3-540-57826-9_134"},{"key":"8_CR10","unstructured":"Homann, K. Symbolisches Loesen mathematischer Probleme durch Kooperation algorithmischer und logischer Systeme. PhD thesis, Univ. of Karlsruhe, 1996."},{"key":"8_CR11","unstructured":"Prawitz, D. Natural Deduction: A Proof-theoretical Study., 1965."},{"key":"8_CR12","unstructured":"Vorkoetter, S. OpenMath specifications: March 1994, March 1994."}],"container-title":["Lecture Notes in Computer Science","Artificial Intelligence and Symbolic Computation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0055905","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,20]],"date-time":"2019-04-20T05:09:17Z","timestamp":1555736957000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0055905"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540649601","9783540498162"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/bfb0055905","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1998]]}}}