{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T12:06:09Z","timestamp":1749125169126},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540664635"},{"type":"electronic","value":"9783540482567"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48256-3_13","type":"book-chapter","created":{"date-parts":[[2007,8,3]],"date-time":"2007-08-03T20:15:22Z","timestamp":1186172122000},"page":"185-202","source":"Crossref","is-referenced-by-count":7,"title":["On the Implementation of an Extensible Declarative Proof Language"],"prefix":"10.1007","author":[{"given":"Vincent","family":"Zammit","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[1999,9,17]]},"reference":[{"key":"13_CR1","unstructured":"Bruno Barras et al. The Coq Proof Assistant Reference Manual. Projet Coq-INRIA-Rocquencourt, CNRS-ENS Lyons, November 1996. (Version 6.1)."},{"issue":"1","key":"13_CR2","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1023\/A:1005996623714","volume":"20","author":"A. Degtyarev","year":"1998","unstructured":"Anatoli Degtyarev and Andrei Voronkov. What you always wanted to know about rigid E-unification. Journal of Automated Reasoning, 20(1):47\u201380, 1998.","journal-title":"Journal of Automated Reasoning"},{"key":"13_CR3","unstructured":"M. J. C. Gordon and T. F. Melham. Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Cambridge University Press, 1993."},{"key":"13_CR4","volume-title":"Proceedings of the Third HOL Users Meeting","author":"E. Gunter","year":"1990","unstructured":"Elsa Gunter. The implementation and use of abstract theories in HOL. In Proceedings of the Third HOL Users Meeting, Computer Science Department, Aarhus University, Ny Munkegade, Building 540, DK-8000 Aarhus C, Denmark, October 1990. Technical Report DAIMI PB-340 (December 1990)."},{"key":"13_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1007\/BFb0105406","volume-title":"Proceedings of the 9th International Conference on Theorem Proving in Higher Order Logics (TPHOLs\u201996)","author":"J. Harrison","year":"1996","unstructured":"J. Harrison. A Mizar mode for HOL. In von Wright et al. J. Grundy, and J. Harrison, editors. Proceedings of the 9th International Conference on Theorem Proving in Higher Order Logics (TPHOLs\u201996), volume 1125 of Lecture Notes in Computer Science, Turku, Finland, August 1996 [16], pages 203\u2013220."},{"key":"13_CR6","volume-title":"Topics in Algebra","author":"I.N. Herstein","year":"1975","unstructured":"I.N. Herstein. Topics in Algebra. John Wiley & Sons, New York, 2nd edition, 1975.","edition":"2nd edition"},{"key":"13_CR7","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"315","DOI":"10.1007\/BFb0105413","volume-title":"Proceedings of the 9th International Conference on Theorem Proving in Higher Order Logics (TPHOLs\u201996)","author":"L. Laibinis","year":"1996","unstructured":"L. Laibinis. Using lattice theory in higher order logic. In von Wright et al. J. Grundy, and J. Harrison, editors. Proceedings of the 9th International Conference on Theorem Proving in Higher Order Logics (TPHOLs\u201996), volume 1125 of Lecture Notes in Computer Science, Turku, Finland, August 1996 [16], pages 315\u2013330."},{"key":"13_CR8","doi-asserted-by":"crossref","unstructured":"David A. Plaisted. Equational reasoning and term rewriting systems. In D. Gabbay, C. Hogger, J. A. Robinson, and J. Siekmann, editors, Handbook of Logic in Artificial Intelligence and Logic Programming, volume 1, chapter 5, pages 273\u2013364. Oxford University Press, Oxford, 1993.","DOI":"10.1093\/oso\/9780198537458.003.0005"},{"key":"13_CR9","unstructured":"Piotr Rudnicki. An overview of the MIZAR project. Available by ftp from http:\/\/www.menaik.cs.ualberta.ca as http:\/\/www.pub\/Mizar\/Mizar_Over.tar.Z. , June 1992."},{"key":"13_CR10","unstructured":"Piotr Rudnicki and Andrzej Trybulec. On equivalents of well-foundedness. Available on the web at http:\/\/www.cs.ualberta.ca\/~piotr\/Mizar\/Wfnd\/ , January 1997."},{"key":"13_CR11","unstructured":"Konrad Slind. Object language embedding in Standard ML of New Jersey. In Proceedings of the Second ML Workshop held at Carnegie Mellon University, Pittsburgh, Pennsylvania, Septermber 26\u201427, 1991, CMU SCS Technical Report, November 1991."},{"key":"13_CR12","volume-title":"Technical Report 416","author":"D. Syme","year":"1997","unstructured":"Don Syme. DECLARE: A prototype declarative proof system for higher order logic. Technical Report 416, University of Cambridge Computer Laboratory, New Museums Site, Pembroke Street, Cambridge, CB2 3QG, UK, 1997."},{"key":"13_CR13","volume-title":"Technical Report 427","author":"D. Syme","year":"1997","unstructured":"Don Syme. Proving Java type soundness. Technical Report 427, University of Cambridge Computer Laboratory, New Museums Site, Pembroke Street, Cambridge, CB2 3QG, UK, 1997."},{"key":"13_CR14","unstructured":"Donald Syme. Declarative Theorem Proving for Operating Semantics. PhDthesis, University of Cambridge, 1998. Submitted for Examination."},{"key":"13_CR15","first-page":"136","volume":"6","author":"A. Trybulec","year":"1978","unstructured":"A. Trybulec. The Mizar-QC\/6000 logic information language. Bulletin of the Association for Literary and Linguistic Computing, 6:136\u2013140, 1978.","journal-title":"Bulletin of the Association for Literary and Linguistic Computing"},{"key":"13_CR16","series-title":"Lect Notes Comput Sci","volume-title":"Proceedings of the 9th International Conference on Theorem Proving in Higher Order Logics (TPHOLs\u201996)","year":"1996","unstructured":"J. von Wright, J. Grundy, and J. Harrison, editors. Proceedings of the 9th International Conference on Theorem Proving in Higher Order Logics (TPHOLs\u201996), volume 1125 of Lecture Notes in Computer Science, Turku, Finland, August 1996. Springer."},{"key":"13_CR17","unstructured":"Vincent Zammit. On the Readability of Machine Checkable Formal Proofs. PhD thesis, University of Kent at Canterbury, October 1998. Submitted for Publication. (Currently available on the world wide web at the http:\/\/www.cs.ukc.ac.uk\/people\/rpg\/vz1\/thesis.ps.gz )."}],"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-48256-3_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,2,17]],"date-time":"2024-02-17T07:30:15Z","timestamp":1708155015000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48256-3_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540664635","9783540482567"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/3-540-48256-3_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1999]]}}}