{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T21:11:37Z","timestamp":1725484297353},"publisher-location":"Berlin, Heidelberg","reference-count":12,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540440390"},{"type":"electronic","value":"9783540456858"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45685-6_12","type":"book-chapter","created":{"date-parts":[[2007,5,19]],"date-time":"2007-05-19T20:47:53Z","timestamp":1179607673000},"page":"164-181","source":"Crossref","is-referenced-by-count":1,"title":["Free-Style Theorem Proving"],"prefix":"10.1007","author":[{"given":"David","family":"Delahaye","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,7,25]]},"reference":[{"key":"12_CR1","unstructured":"Thierry Coquand, Catarina Coquand, Thomas Hallgren, and Aarne Ranta. The Alfa Home Page, 2001. http:\/\/www.md.Chalmers.se\/~hallgren\/Alfa\/ ."},{"key":"12_CR2","series-title":"Lect Notes Comput Sci","volume-title":"Proceedings of Int. Gonf. on Logical Aspects of Computational Linguistics (LAGL), Nancy","author":"Y. Coscoy","year":"1996","unstructured":"Yann Coscoy. A Natural Language Explanation for Formal Proofs. In C. Retor\u00e9, editor, Proceedings of Int. Gonf. on Logical Aspects of Computational Linguistics (LAGL), Nancy, volume 1328. Springer-Verlag LNCS\/LNAI, September 1996."},{"key":"12_CR3","unstructured":"Judy Crow, Sam Owre, John Rushby, Natarajan Shankar, and Mandayam Srivas. A Tutorial Introduction to PVS. In Workshop on Industrial-Strength Formal Specification Techniques, Boca Raton, Florida, April 1995."},{"key":"12_CR4","series-title":"Coq. PhD thesis","volume-title":"Conception de langages pour d\u00e9crire les preuves et les automatisations dans les outils d\u2019aide \u00e0 la preuve: une \u00e9tude dans le cadre du syst\u00e8me","author":"D. Delahaye","year":"2001","unstructured":"David Delahaye. Conception de langages pour d\u00e9crire les preuves et les automatisations dans les outils d\u2019aide \u00e0 la preuve: une \u00e9tude dans le cadre du syst\u00e8me Coq. PhD thesis, Universit\u00e9 Pierre et Marie Curie (Paris 6), D\u00e9cembre 2001."},{"key":"12_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/BFb0097791","volume-title":"Types for Proofs and Programs: International Workshop TYPES\u201996","author":"J. Harrison","year":"1996","unstructured":"John Harrison. Proof Style. In Eduardo Gim\u00e9nez and Christine Paulin-Mohring, editors, Types for Proofs and Programs: International Workshop TYPES\u201996, volume 1512 of LNCS, pages 154\u2013172, Aussois, France, 1996. Springer-Verlag."},{"key":"12_CR6","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"203","DOI":"10.1007\/BFb0105406","volume-title":"Theorem Proving in Higher Order Logics: TPHOLs\u201996","author":"J. Harrison","year":"1996","unstructured":"John Harrison. A Mizar Mode for HOL. In J. von Wright, J. Grundy, and J. Harrison, editors, Theorem Proving in Higher Order Logics: TPHOLs\u201996, volume 1125 of LNCS, pages 203\u2013220, 1996."},{"key":"12_CR7","unstructured":"Lena Magnusson. The Implementation of ALF\u2014a Proof Editor Based on Martin-L\u00f6f\u2019s Monomorphic Type Theory with Explicit Substitution. PhD thesis, Chalmers University of Technology, 1994."},{"key":"12_CR8","doi-asserted-by":"crossref","unstructured":"Don Syme. Declarative Theorem Proving for Operational Semantics. PhD thesis, University of Cambridge, 1998.","DOI":"10.1007\/3-540-48256-3_14"},{"key":"12_CR9","unstructured":"The Coq Development Team. The Coq Proof Assistant Reference Manual Version 1.3. INRIA-Rocquencourt, May 2002. http:\/\/coq.inria.fr\/doc-eng.html ."},{"key":"12_CR10","first-page":"136","volume":"6","author":"A. Trybulec","year":"1978","unstructured":"Andrzej Trybulec. The Mizar-QC\/6000 logic information language. In ALLC Bulletin (Association for Literary and Linguistic Computing), volume 6, pages 136\u2013140, 1978.","journal-title":"ALLC Bulletin (Association for Literary and Linguistic Computing)"},{"key":"12_CR11","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/3-540-48256-3_12","volume-title":"Theorem Proving in Higher Order Logics: TPHOLs\u201999","author":"M. Wenzel","year":"1999","unstructured":"Markus Wenzel. Isar-A Generic Interpretative Approach to Readable Formal Proof Documents. In Yves Bertot, Gilles Dowek, Andr\u00e9 Hirschowitz, Christine Paulin-Mohring, and Laurent Th\u00e9ry, editors, Theorem Proving in Higher Order Logics: TPHOLs\u201999, volume 1690 of LNCS, pages 167\u2013184. Springer-Verlag, 1999."},{"key":"12_CR12","series-title":"PhD thesis","volume-title":"On the Readability of Machine Checkable Formal Proofs","author":"V. Zammit","year":"1998","unstructured":"Vincent Zammit. On the Readability of Machine Checkable Formal Proofs. PhD thesis, University of Kent, Canterbury, October 1998."}],"container-title":["Lecture Notes in Computer Science","Theorem Proving in Higher Order Logics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45685-6_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,28]],"date-time":"2019-04-28T05:38:19Z","timestamp":1556429899000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45685-6_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540440390","9783540456858"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/3-540-45685-6_12","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}