{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T13:28:03Z","timestamp":1725456483169},"publisher-location":"Berlin\/Heidelberg","reference-count":19,"publisher":"Springer-Verlag","isbn-type":[{"type":"print","value":"354057235X"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/bfb0013180","type":"book-chapter","created":{"date-parts":[[2005,11,23]],"date-time":"2005-11-23T07:23:18Z","timestamp":1132730598000},"page":"229-240","source":"Crossref","is-referenced-by-count":3,"title":["GLEFATINF:A graphic framework for combining theorem provers and editing proofs for different logics"],"prefix":"10.1007","author":[{"given":"Ricardo","family":"Caferra","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michel","family":"Herment","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"18_CR1","doi-asserted-by":"publisher","first-page":"285","DOI":"10.1007\/BF00243811","volume":"7","author":"P.B. Andrews","year":"1991","unstructured":"[And91] P.B. Andrews: More on the problem of finding a mapping between clause representation and natural deduction representation, Journal of Automated Reasoning 7 (1991), pp. 285\u2013286.","journal-title":"Journal of Automated Reasoning"},{"key":"18_CR2","doi-asserted-by":"publisher","first-page":"309","DOI":"10.1007\/BF00245294","volume":"9","author":"A. Avron","year":"1992","unstructured":"[AHMP92] A. Avron, F.A. Honsell, I.A. Mason, R. Pollack: Using typed lambda calculus to implement formal systems on a machine, Journal of Automated Reasoning 9 (1992), pp. 309\u2013354.","journal-title":"Journal of Automated Reasoning"},{"key":"18_CR3","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1016\/0890-5401(91)90023-U","volume":"92","author":"A. Avron","year":"1991","unstructured":"[Avr91] A. Avron: Simple consequence relations, Information and Computation 92 (1991), pp. 105\u2013139.","journal-title":"Information and Computation"},{"key":"18_CR4","unstructured":"[BC87] T. Boy de la Tour, R. Caferra: Proof analogy in interactive theorem proving: a method to use and express it via second order pattern matching, Proc. AAAI-87, Morgan & Kaufmann 1987, pp. 95\u201399."},{"key":"18_CR5","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1016\/0890-5401(88)90005-3","volume":"76","author":"T. Coquand","year":"1988","unstructured":"[CH88] T. Coquand, G. Huet: The calculus of constructions, Information and Computation 76 (1988), pp. 95\u2013120.","journal-title":"Information and Computation"},{"key":"18_CR6","unstructured":"[CH93] R. Caferra, M. Herment: GLEFATINF A graphic framework for combining provers and editing proofs for different logics, (long version). In preparation."},{"key":"18_CR7","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1016\/0004-3702(76)90007-2","volume":"7","author":"D. Chester","year":"1976","unstructured":"[Che76] D. Chester: The translation of formal proofs into English, Artificial Intelligence 7 (1976), pp. 261\u2013278.","journal-title":"Artificial Intelligence"},{"key":"18_CR8","doi-asserted-by":"crossref","unstructured":"[CHZ91] R. Caferra, M. Herment, N. Zabel: User-oriented theorem proving with the ATINF graphic proof editor, Proc. FAIR'91, LNAI 535, Springer-Verlag 1991, pp. 2\u201310.","DOI":"10.1007\/3-540-54507-7_1"},{"key":"18_CR9","doi-asserted-by":"crossref","unstructured":"[CZ92] E. Clarke, X. Zhao: Analytica-An experiment in combinig theorem proving and symbolic computation, RR CMU-CS-92-117, September 1992.","DOI":"10.21236\/ADA258656"},{"key":"18_CR10","unstructured":"[Dyb82] P. Dybjer: Mathematical proofs in natural language, Report 5, Programming Methodology Group, University of Goteborg, April 1982."},{"key":"18_CR11","unstructured":"[HHP89] R. Harper, F. Honsell, G. Plotkin: A framework for defining logics, RR CMU-CS-89-173, Carnegie Mellon University, January 1989."},{"key":"18_CR12","unstructured":"[Hua90] X. Huang: Reference choices in mathematical proofs, Proc. ECAI'90, Pitman 1990, pp. 720\u2013725."},{"key":"18_CR13","unstructured":"[Lin90] C. Lingenfelder: Transformation and structuring of computer generated proofs, SEKI Report SR-90-26, University of Kaiserslautern 1990."},{"key":"18_CR14","unstructured":"[LP90] C. Lingenfelder, A. Pr\u00e4cklein: Presentation of proofs in equational calculus, SEKI Report SR-90-15 (SFB), University of Kaiserslautern 1990."},{"key":"18_CR15","volume-title":"Technical Report ANL-90\/9","author":"W.W. McCune","year":"1990","unstructured":"[McC90] W.W. McCune: OTTER 2.0 users guide, Technical Report ANL-90\/9, Argonne National Laboratory, Illinois 1990."},{"key":"18_CR16","doi-asserted-by":"crossref","unstructured":"[Mil84] D.A. Miller: Expansion tree proofs and their conversion to natural deduction, Proc. CADE-7, LNCS 170, Springer-Verlag 1984, pp. 375\u2013393.","DOI":"10.1007\/978-0-387-34768-4_22"},{"key":"18_CR17","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1007\/BF00248324","volume":"5","author":"L.C. Paulson","year":"1989","unstructured":"[Pau89] L.C. Paulson: The foundation of a generic theorem prover, Journal of Automated Reasoning 5 (1989), pp. 363\u2013397.","journal-title":"Journal of Automated Reasoning"},{"key":"18_CR18","unstructured":"[Qui87] V. Quint: Une approche de l'Edition Structur\u00e9e des documents, Ph.D Thesis, Universit\u00e9 Sc. Tech. et M\u00e9d. de Grenoble (1987)."},{"key":"18_CR19","doi-asserted-by":"crossref","unstructured":"[Wang93] D.M. Wang: An elimination method based on Seidenberg's theory and its applications in computational algebraic geometry In Progress in Mathematics 109, pp. 301\u2013328, Birkh\u00e4user, 1993.","DOI":"10.1007\/978-1-4612-2752-6_21"}],"container-title":["Lecture Notes in Computer Science","Design and Implementation of Symbolic Computation Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/www.springerlink.com\/index\/pdf\/10.1007\/BFb0013180","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,11]],"date-time":"2020-04-11T04:32:31Z","timestamp":1586579551000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0013180"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["354057235X"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/bfb0013180","relation":{},"subject":[]}}