{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,4]],"date-time":"2022-04-04T11:23:00Z","timestamp":1649071380188},"reference-count":26,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[1992,3,1]],"date-time":"1992-03-01T00:00:00Z","timestamp":699408000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["BIT"],"published-print":{"date-parts":[[1992,3]]},"DOI":"10.1007\/bf01995105","type":"journal-article","created":{"date-parts":[[2005,8,10]],"date-time":"2005-08-10T14:40:23Z","timestamp":1123684823000},"page":"15-29","source":"Crossref","is-referenced-by-count":2,"title":["Theo: An interactive proof development system"],"prefix":"10.1007","volume":"32","author":[{"given":"Jo\u00eblle","family":"Despeyroux","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"BF01995105_CR1","unstructured":"A. Avron,Simple Consequence Relations, Edinburgh Report ECS-LFCS-87-30, June 1987."},{"key":"BF01995105_CR2","unstructured":"A. Avron, F. Honsell, A. Mason,Using typed \u03bb-calculus to implement formal systems on a machine, Edinburgh Report ECS-LFCS-87-31, July 1987."},{"key":"BF01995105_CR3","volume-title":"The Handbook of Mathematical Logic","author":"J. Barwise","year":"1977","unstructured":"J. Barwise,The Handbook of Mathematical Logic, North-Holland, Amsterdam, 1977, reprinted in 1983."},{"key":"BF01995105_CR4","unstructured":"Th. Coquand,An analysis of Girard's paradox, Proc. of the first ACM-IEEE Symp. on Logic In Computer Science, Cambridge, Ma, USA, June 1986."},{"key":"BF01995105_CR5","unstructured":"Th. Coquand,The tactics Theorem Prover, User's guide, inCalculus of Constructions, Documentation and Users' guide, Version 4.10, July 1st 1989."},{"key":"BF01995105_CR6","unstructured":"R. L. Constable et al.,Implementing Mathematics with the Nuprl Proof Development System, Prentice-Hall, 1986."},{"key":"BF01995105_CR7","unstructured":"J. Despeyroux,Proof of translation in natural semantics, Inria Research Report 514, april 1986, also in the Proc. of the first ACM-IEEE Symp. on Logic In Computer Science, Cambridge, Ma, USA, June 1986."},{"key":"BF01995105_CR8","unstructured":"J. Despeyroux,First experiments with theorem proving in Centaur: the Calculus of Constructions, the Edinburgh Logical Framework, and Theo, in Esprit project 348 GIPE. Third annual review report, January 1988."},{"key":"BF01995105_CR9","unstructured":"J. Despeyroux,Theo: an interactive Typol theorem prover, Inria Research Report 887, August 1988."},{"key":"BF01995105_CR10","unstructured":"Th. Despeyroux,Typol: a formalism to implement Natural Semantics, Inria Technical Report 94, mars 1988."},{"key":"BF01995105_CR11","unstructured":"A. Felty and D. Miller,Specifying theorem provers in a higher-order logic programming language, Ninth Conference on Automated Deduction, 1988, and Report MS-CIS-88-12, University of Pennsylvania, February 1988."},{"key":"BF01995105_CR12","volume-title":"Studies in Logic and the Foundations of Mathematics","author":"G. Gentzen","year":"1969","unstructured":"G. Gentzen,The Collected Papers of Gerhard Gentzen, edited by M. E. Szabo, inStudies in Logic and the Foundations of Mathematics, North-Holland, Amsterdam, 1969."},{"key":"BF01995105_CR13","unstructured":"T. G. Griffin,An Environment for Formal Systems, Report 087-022005, Cornell University, August 1987."},{"key":"BF01995105_CR14","unstructured":"R. Harper, F. Honsell and G. Plotkin,A Framework for defining Logics, Proc. of the second ACM-IEEE Symp. on Logic In Computer Science, Cornell, USA, 1987."},{"key":"BF01995105_CR15","unstructured":"L. Hasco\u00ebt,A tactic-driven system for building proofs, Inria Research report 770, Dec. 1987. Also in the Proc. of the 7th seminarProgrammation en Logique, Tregastel, May 1988."},{"key":"BF01995105_CR16","unstructured":"G. Huet,A uniform approach to Type Theory, Inria Research Report 795, February 1988."},{"key":"BF01995105_CR17","unstructured":"J. P. Jouannaud and C.Kirchner,Solving Equations in Abstract Algebras: A Rule-Bases survey of Unification. March 31, 1990."},{"key":"BF01995105_CR18","doi-asserted-by":"crossref","unstructured":"G. Kahn,Natural Semantics, Proc. of Symp. on Theoretical Aspects of Computer Science, Passau, Germany, February 1987, also Inria Research Report 601, Feb. 1987.","DOI":"10.1007\/BFb0039592"},{"key":"BF01995105_CR19","unstructured":"D. Miller and G. Nadathur,A logic programming approach to manipulating formulas and programs, Report MS-CIS-87-113, University of Pennsylvania, December 1987."},{"key":"BF01995105_CR20","unstructured":"G. Nadathur,A higher-order logic as the basis for logic programming, Ph.D. dissertation, University of Pennsylvania, Dec. 1986, also Report MS-CIS-87-48, University of Pennsylvania, June 1987."},{"key":"BF01995105_CR21","doi-asserted-by":"crossref","unstructured":"L. C. Paulson,Logic and computation. Interactive proof with Cambridge LCF, Cambridge Tracts in Theoretical Computer Science 2, 1987.","DOI":"10.1017\/CBO9780511526602"},{"key":"BF01995105_CR22","unstructured":"L. C. Paulson,The representation of logics in higher-order logic, Cambridge Technical Report 113, 1987."},{"key":"BF01995105_CR23","first-page":"363","volume":"5","author":"L. C. Paulson","year":"1989","unstructured":"L. C. Paulson,The foundation of a generic theorem prover, Cambridge Technical Report 130, March 1988 and Journal of Automated Reasoning, vol. 5, 1989, pp. 363\u2013397.","journal-title":"Cambridge Technical Report 130, March 1988 and Journal of Automated Reasoning"},{"key":"BF01995105_CR24","unstructured":"G. D. Plotkin,A structural approach to operational semantics, Aarhus Report DAIMI FN-19, 1981."},{"key":"BF01995105_CR25","volume-title":"Natural Deduction, a Proof-Theoretical Study","author":"D. Prawitz","year":"1965","unstructured":"D. Prawitz,Natural Deduction, a Proof-Theoretical Study, Almqvist & Wiksell, Stockholm, 1965."},{"key":"BF01995105_CR26","doi-asserted-by":"crossref","unstructured":"D. Prawitz,Ideas and results in Proof Theory, Proc. of the 2nd. Scand. Logic Congress, North Holland, 1971.","DOI":"10.1016\/S0049-237X(08)70849-8"}],"container-title":["BIT"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01995105.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF01995105\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01995105","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,8]],"date-time":"2020-04-08T20:25:48Z","timestamp":1586377548000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF01995105"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1992,3]]},"references-count":26,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1992,3]]}},"alternative-id":["BF01995105"],"URL":"https:\/\/doi.org\/10.1007\/bf01995105","relation":{},"ISSN":["0006-3835","1572-9125"],"issn-type":[{"value":"0006-3835","type":"print"},{"value":"1572-9125","type":"electronic"}],"subject":[],"published":{"date-parts":[[1992,3]]}}}