{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T12:46:21Z","timestamp":1725453981743},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540638889"},{"type":"electronic","value":"9783540696612"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1997]]},"DOI":"10.1007\/bfb0000460","type":"book-chapter","created":{"date-parts":[[2005,10,5]],"date-time":"2005-10-05T10:30:36Z","timestamp":1128508236000},"page":"16-29","source":"Crossref","is-referenced-by-count":0,"title":["Head-tactics simplification"],"prefix":"10.1007","author":[{"given":"Yves","family":"Bertot","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,9,7]]},"reference":[{"key":"2_CR1","doi-asserted-by":"crossref","unstructured":"Janet Bertot and Yves Bertot. CtCoq: A system presentation. In Automated Deduction (CADE-13), volume 1104 of Lecture Notes in Artificial Intelligence, pages 231\u2013234. Springer-Verlag, July 1996.","DOI":"10.1007\/3-540-61511-3_85"},{"key":"2_CR2","doi-asserted-by":"crossref","unstructured":"Yves Bertot, Gilles Kahn, and Laurent Th\u00e9ry. Proof by pointing. In Theoretical Aspects of Computer Software, volume 789 of Lecture Notes in Computer Science, pages 141\u2013160, 1994.","DOI":"10.1007\/3-540-57887-0_94"},{"key":"2_CR3","unstructured":"Yves Bertot, Thomas Schreiber, and Dilip Sequeira. Proof by pointing in a weakly structured context. ftp:\/\/ftp.dcs.ed.ac.uk\/pub\/lego\/pbp\/main.ps."},{"key":"2_CR4","unstructured":"Yves Bertot and Laurent Th\u00e9ry. A generic approach to building user interfaces for theorem provers. To appear in Journal of Symbolic Computation."},{"key":"2_CR5","doi-asserted-by":"crossref","unstructured":"Patrick Borras, Dominique Cl\u00e9ment, Thierry Despeyroux, Janet Incerpi, Gilles Kahn, Bernard Lang, and Val\u00e9rie Pascual. Centaur: the system. In Third Symposium on Software Development Environments, 1988. (Also appears as INRIA Report no. 777).","DOI":"10.1145\/64135.65005"},{"key":"2_CR6","unstructured":"Debra Cameron and Bill Rosenblatt. Learning GNU Emacs. O'Reilly & Associates, Inc., 1991."},{"key":"2_CR7","unstructured":"Robert Constable, S. F. Allen, H. M. Bromley, W. R. Cleaveland, J. F. Cremer, R. W. Harber, D. J. Howe, T. B. Knoblock, N. P. Mendler, P. Panangaden, J. T. Sasaki, and S. F. Smith. Implementing mathematics with the Nuprl proof development system. Prentice-Hall, 1986."},{"key":"2_CR8","unstructured":"Amy Felty. Specifying and Implementing Theorem Provers in a Higher-Order Logic Programming Language. PhD thesis, University of Pennsylvania, 1989."},{"key":"2_CR9","doi-asserted-by":"crossref","unstructured":"Amy Felty and Douglas Howe. Tactic theorem proving with refinement-tree proofs and metavariables. In Automated Deduction(CADE-12), volume 814 of Lecture Notes in Computer Science. Springer-Verlag, June 1995.","DOI":"10.1007\/3-540-58156-1_44"},{"key":"2_CR10","unstructured":"Amy Felty and Laurent Th\u00e9ry. Interactive theorem proving with temporal logic. To appear in Journal of Symbolic Computation."},{"key":"2_CR11","unstructured":"Michael Gordon and Thomas Melham. Introduction to HOL: A theorem proving environment for higher order logic. Cambridge University Press, 1993."},{"key":"2_CR12","unstructured":"Timothy Griffin. Notational definition and top-down refinement for interactive proof development systems. PhD thesis, Cornell University, 1988."},{"key":"2_CR13","unstructured":"INRIA. The Coq Proof Assistant Reference Manual, December 1996. Version6.1."},{"key":"2_CR14","unstructured":"The LEGO World Wide Web page. url http:\/\/www.dcs.ed.ac.uk\/home\/lego."},{"key":"2_CR15","doi-asserted-by":"crossref","unstructured":"Lena Magnusson and Bengt Nordstr\u00f6m. The ALF proof editor and its proof engine. In Types for Proofs and Programs, volume 806 of Lecture Notes in Computer Science, pages 213\u2013237. Springer-Verlag, 1994.","DOI":"10.1007\/3-540-58085-9_78"},{"key":"2_CR16","unstructured":"Per Martin-L\u00f6f. Intuitionistic type theories. Bibliopolis, 1984."},{"key":"2_CR17","unstructured":"Robin Milner, Mads Tofte, and Robert Harper. The Definition of Standard ML. MIT Press, 1990. ISBN 0-262-63132-6."},{"key":"2_CR18","doi-asserted-by":"crossref","unstructured":"Lawrence C. Paulson. Logic and computation, Interactive proof with Cambridge LCF. Cambridge University Press, 1987.","DOI":"10.1017\/CBO9780511526602"},{"key":"2_CR19","unstructured":"Lawrence C. Paulson. ML for the working programmer. Cambridge University Press, 1991."},{"key":"2_CR20","doi-asserted-by":"crossref","unstructured":"Lawrence C. Paulson and Tobias Nipkow. Isabelle: a generic theorem prover, volume 828 of Lecture Notes in Computer Science. Springer-Verlag, 1994.","DOI":"10.1007\/BFb0030541"},{"key":"2_CR21","doi-asserted-by":"crossref","unstructured":"Laurent Th\u00e9ry. A proof development system for the HOL theorem prover. In Higher Order Logic theorem proving and its applications, volume 780 of Lecture Notes in Computer Science. Springer-Verlag, August 1993.","DOI":"10.1007\/3-540-57826-9_129"},{"key":"2_CR22","doi-asserted-by":"crossref","unstructured":"Laurent Th\u00e9ry, Yves Bertot, and Gilles Kahn. Real Theorem Provers Deserve Real User-Interfaces. Software Engineering Notes, 17(5), 1992. Proceedings of the 5th Symposium on Software Development Environments.","DOI":"10.1145\/142868.143760"}],"container-title":["Lecture Notes in Computer Science","Algebraic Methodology and Software Technology"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0000460","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,10]],"date-time":"2020-04-10T02:21:35Z","timestamp":1586485295000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0000460"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997]]},"ISBN":["9783540638889","9783540696612"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/bfb0000460","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1997]]}}}