{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T15:57:36Z","timestamp":1725638256024},"publisher-location":"Vienna","reference-count":26,"publisher":"Springer Vienna","isbn-type":[{"type":"print","value":"9783211829004"},{"type":"electronic","value":"9783709174913"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/978-3-7091-7491-3_17","type":"book-chapter","created":{"date-parts":[[2011,12,5]],"date-time":"2011-12-05T05:34:51Z","timestamp":1323063291000},"page":"330-346","source":"Crossref","is-referenced-by-count":2,"title":["Evaluating the Interfaces of Three Theorem Proving Assistants"],"prefix":"10.1007","author":[{"given":"Nicholas A.","family":"Merriam","sequence":"first","affiliation":[]},{"given":"Michael D.","family":"Harrison","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"17_CR1","unstructured":"J. S. Aitken, P. Gray, T. Melham, and M. Thomas. A Study of User Activity in Interactive Theorem Proving. Submitted to J. Symbolic Computing."},{"key":"17_CR2","doi-asserted-by":"crossref","unstructured":"W. M. Farmer, J. D. Guttman, and F. J. Thayer. Little theories. In Kapur [8], pages 567\u2013581.","DOI":"10.1007\/3-540-55602-8_192"},{"key":"17_CR3","unstructured":"W. M. Farmer, J. D. Guttman, and F. J. Thayer. The IMPS User\u2019s Maunual. The MITRE Corporation, 1994."},{"key":"17_CR4","unstructured":"G. Gentzen. Investigations into logical deduction. In M. E. Szabo, editor, The Collected Papers of Gerhard Gentzen. North-Holland, 1969."},{"key":"17_CR5","unstructured":"D. J. Gilmore. Structural Visibility and Program Comprehension. In M. D. Harrison and A. F. Monk, editors, People and Computers: Designing for Usability, BCS Workshop series, pages 527\u2013545. Cambridge University Press, 1986."},{"key":"17_CR6","unstructured":"Li Gong, Patrick Lincoln, and John Rushby. Byzantine agreement with authentication: Observations and applications in tolerating hybrid and link faults. In Dependable Computing for Critical Applications\u20145, pages 79\u201390, Champaign, IL, September 1995. IFIP WG 10.4, preliminary proceedings."},{"key":"17_CR7","unstructured":"J.-M. Hoc, T. R. G. Green, R. Samur\u00e7ay, and D. J. Gilmore, editors. Psychology of Programming. Computers and People. Academic Press, 1990."},{"key":"17_CR8","doi-asserted-by":"crossref","unstructured":"D. Kapur, editor. Automated Deduction \u2014 CADE 11, volume 607 of Lecture Notes in Computer Science. Springer-Verlag, 1992.","DOI":"10.1007\/3-540-55602-8"},{"issue":"3","key":"17_CR9","doi-asserted-by":"publisher","first-page":"274","DOI":"10.2307\/749516","volume":"20","author":"D Kirshner","year":"1989","unstructured":"D. Kirshner. The Visual Syntax of Algebra. Journal for Research in Mathematical Education, 20(3):274\u2013287, 1989.","journal-title":"Journal for Research in Mathematical Education"},{"key":"17_CR10","unstructured":"Leslie Lamport. How to Write a Long Formula. Online at http:\/\/www.research.digital.com\/SRC\/proofs\/proofs.html, 1993."},{"key":"17_CR11","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1111\/j.1551-6708.1987.tb00863.x","volume":"11","author":"JH Larkin","year":"1987","unstructured":"J. H. Larkin and H. A. Simon. Why a Diagram is (Sometimes) Worth Ten Thousand Words. Cognitive Science, 11:65\u201399, 1987.","journal-title":"Cognitive Science"},{"key":"17_CR12","unstructured":"W. N. Dember and J. S. Warm. Psychology of Perception, chapter 7: Perception of Form. Holt, Rinehart and Winston, 1979."},{"key":"17_CR13","unstructured":"W. M. Newman and M. G. Lamming. Interactive System Design. Addison-Wesley, 1995."},{"key":"17_CR14","doi-asserted-by":"crossref","unstructured":"J. Nicholls. Z Notation: version 1.2. Technical report, Z Standards Panel, University of Oxford, Sept. 1995.","DOI":"10.21236\/ADA388235"},{"key":"17_CR15","doi-asserted-by":"crossref","unstructured":"D. C. Oppen. Pretty-printing. ACM Transactions on Programming Languages, 2(4), Oct. 1980.","DOI":"10.1145\/357114.357115"},{"key":"17_CR16","doi-asserted-by":"crossref","unstructured":"S._Owre, J. Rushby, and N. Shankar. PVS: A Prototype Verification System. In Kapur [8], pages 748\u2013752.","DOI":"10.1007\/3-540-55602-8_217"},{"key":"17_CR17","doi-asserted-by":"crossref","unstructured":"Philippe Palanque. Towards an integrated proposal for Interactive Systems design based on TLIM and ICO. In F. Bodart and J. Vanderdonckt, editors, Eurographics Workshop on Design, Specification and Verification of Interactive Systems: Informal Proceedings, pages 69\u201385, Belgium, 1996. Computer Science Dept. U. Namur.","DOI":"10.1007\/978-3-7091-7491-3_9"},{"key":"17_CR18","unstructured":"G. Polya. How To Solve It. Princeton University Press, second edition, 1957."},{"issue":"3","key":"17_CR19","doi-asserted-by":"crossref","first-page":"257","DOI":"10.1109\/TSMC.1983.6313160","volume":"13","author":"J Rasmussen","year":"1983","unstructured":"J. Rasmussen. Skills, Rules and Knowledge; signals, signs and symbols, and other distinctions in human performance models. IEEE Transactions on Systems, Man and Cybernetics, 13(3):257\u2013266, 1983.","journal-title":"IEEE Transactions on Systems, Man and Cybernetics"},{"key":"17_CR20","doi-asserted-by":"crossref","unstructured":"John Rushby. Design choices in specification languages and verification systems. In Phillip Windley, editor, International Workshop on the HOL Theorem Proving System and its Applications, pages 195\u2013204. IEEE Computer Society, 1991.","DOI":"10.1109\/HOL.1991.596287"},{"key":"17_CR21","unstructured":"N. Shankar, S. Owre, and J. Rushby. The PVS Proof Checker: A Reference Manual SRI International, 1995."},{"issue":"4","key":"17_CR22","doi-asserted-by":"publisher","first-page":"529","DOI":"10.1145\/322033.322034","volume":"24","author":"R Shostak","year":"1977","unstructured":"R. Shostak. On the SUP-INF method for proving Presburger formulas. Journal of the ACM, 24(4):529\u2013543, Oct. 1977.","journal-title":"Journal of the ACM"},{"key":"17_CR23","unstructured":"J. M. Spivey. The Z Notation. Prentice Hall International, 2nd edition, 1992."},{"key":"17_CR24","unstructured":"E. Swanson. Mathematics into Type. American Mathematical Society, 1971."},{"key":"17_CR25","unstructured":"I. Toyn and J. Hall. Proving Conjectures using Cadiz. University of York, 1995."},{"key":"17_CR26","doi-asserted-by":"crossref","unstructured":"J. C. P. Woodcock and S. M. Brien. W: A logic for Z. In J. E. Nicholls, editor, Z User Workshop, York 1991, Workshops in Computing, pages 77\u201396. Springer-Verlag, 1992.","DOI":"10.1007\/978-1-4471-3203-5_4"}],"container-title":["Eurographics","Design, Specification and Verification of Interactive Systems \u201996"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-7091-7491-3_17.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,23]],"date-time":"2020-11-23T09:36:13Z","timestamp":1606124173000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-7091-7491-3_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783211829004","9783709174913"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-7091-7491-3_17","relation":{},"ISSN":["0946-2767"],"issn-type":[{"type":"print","value":"0946-2767"}],"subject":[],"published":{"date-parts":[[1996]]}}}