{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,3,30]],"date-time":"2022-03-30T10:34:51Z","timestamp":1648636491232},"reference-count":18,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[1998,3,1]],"date-time":"1998-03-01T00:00:00Z","timestamp":888710400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Software - Concepts & Tools"],"published-print":{"date-parts":[[1998,3]]},"DOI":"10.1007\/s003780050012","type":"journal-article","created":{"date-parts":[[2002,8,25]],"date-time":"2002-08-25T08:19:44Z","timestamp":1030263584000},"page":"89-95","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Theminimal user interface of a simple refinement tool"],"prefix":"10.1007","volume":"19","author":[{"given":"Philipp","family":"Heuberger","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2014,4,30]]},"reference":[{"key":"4_CR1","volume-title":"B-Technology Technical Overview","author":"J.R. Abrial","year":"1993","unstructured":"Abrial, J.R. et al: B-Technology Technical Overview. B-Core (UK) Ltd. (1993)"},{"key":"4_CR2","volume-title":"Technical Report 65","author":"R. Back","year":"1996","unstructured":"Back, R., Grundy, J., von Wright, J.: Structured Calculational Proof. Technical Report 65, TUCS (1996)"},{"key":"4_CR3","volume-title":"UITP'96","author":"R. Backhouse","year":"1996","unstructured":"Backhouse, R.: Verhoeven, R.: Math\u222bpad: Tool Support for the Calculational Method. In UITP'96, [17], 1996, see http:\/\/dcpu1.cs.york.ac.uk:6666\/~nam\/uitp\/proceedings.html"},{"key":"4_CR4","doi-asserted-by":"crossref","unstructured":"Bertot, Y., Kahn, G., Th\u00e9ry, L.: Proof by Pointing. In STACS'94, number 789 in LNCS 1994","DOI":"10.1007\/3-540-57887-0_94"},{"key":"4_CR5","volume-title":"International Symposium on Symbolic and Algebraic Computation, Maui, Hawaii","author":"B. Buchberger","year":"1997","unstructured":"Buchberger, B. et al.: A Survey on the Theorema Project. In W. Kuechlin, editor, International Symposium on Symbolic and Algebraic Computation, Maui, Hawaii, July 1997"},{"key":"4_CR6","volume-title":"Predicate Calculus and Program Semantics","author":"E.W. Dijkstra","year":"1989","unstructured":"Dijkstra, E.W., Scholten, C.S.: Predicate Calculus and Program Semantics. Springer-Verlag, 1989"},{"key":"4_CR7","volume-title":"Introduction to HOL: A Theorem Proving Environment for Higher Order Logic","author":"M.J.C. Gordon","year":"1993","unstructured":"Gordon, M.J.C., Melham, T.F.: Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Cambridge University Press, 1993"},{"key":"4_CR8","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4757-3837-7","volume-title":"A Logical Approach to Discrete Mathematics","author":"D. Gries","year":"1993","unstructured":"Gries, D., Schneider, F.B.: A Logical Approach to Discrete Mathematics. Springer Verlag, 1993"},{"key":"4_CR9","volume-title":"The Computer Journal","author":"J. Grundy","year":"1996","unstructured":"Grundy, J.: Transformational Hierarchical Reasoning. The Computer Journal, 39(4), (1996)"},{"key":"4_CR10","volume-title":"FME'96","author":"P. Heuberger","year":"1996","unstructured":"Heuberger, P.: Refinement Tool: Refstep. FME'96, Oxford, Tool Demonstration Session, March 1996"},{"key":"4_CR11","first-page":"565","volume-title":"7th Nordic Workshop on Programming Theory, Vol. 86 of G\u00f6teborg University and Chalmers University","author":"P. Heuberger","year":"1995","unstructured":"Heuberger, P., Hofmann D.: The Refinement Tool: RefStep. In Marie Larsson Bror Bjerner and Bengt Nordstr\u00f6m, editors, 7th Nordic Workshop on Programming Theory, Vol. 86 of G\u00f6teborg University and Chalmers University, pp. 565\u2013570, November 1995"},{"key":"4_CR12","volume-title":"Technical Report Series A","author":"T. L\u00e5ngbacka","year":"1995","unstructured":"L\u00e5ngbacka T., Ruk\u0161\u0117nas, R., von Wright, J.: TkWinHOL: A tool for Doing Window Inference in HOL. Technical Report Series A, \u00c5bo Akademi University, Computer Science Department, April 1995"},{"key":"4_CR13","volume-title":"DSV-IS'96","author":"N.A. Merriam","year":"1996","unstructured":"Merriam, N.A., Harrison, M.D.: Evaluating the Interfaces of Three Theorem Proving Assistants. In F. Bodart, J. Vanderdonckt, editors, DSV-IS'96, Springer, 1996"},{"key":"4_CR14","volume-title":"Programming from Specifications","author":"C. Morgan","year":"1994","unstructured":"Morgan, C.: Programming from Specifications. Prentice Hall, 1994"},{"key":"4_CR15","unstructured":"SRI: Overview of the PVS Verification System. http:\/\/www.csl.sri.com\/pvs.html , world-wide web site"},{"key":"4_CR16","volume-title":"UITP'96","author":"I. Toyn","year":"1996","unstructured":"Toyn, I.: Formal Reasoning in the Z Notation Using CADiZ. In UITP'96 [17], 1996, http:\/\/dcpu1.cs.york.ac.uk:6666\/~nam\/uitp\/proceedings.html"},{"key":"4_CR17","unstructured":"University of York: User Interfaces for Theorem Provers. 1996 http:\/\/dcpu1.cs.york.ac.uk:6666\/~nam\/uitp\/proceedings.html"},{"key":"4_CR18","volume-title":"Project Oberon: the Design of an Operating System and Compiler","author":"N. Wirth","year":"1992","unstructured":"Wirth, N., Gutknecht, J.: Project Oberon: the Design of an Operating System and Compiler. Addison Wesley, 1992"}],"container-title":["Software - Concepts & Tools"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s003780050012.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s003780050012\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s003780050012","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,28]],"date-time":"2019-05-28T15:15:46Z","timestamp":1559056546000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s003780050012"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998,3]]},"references-count":18,"journal-issue":{"issue":"2","published-print":{"date-parts":[[1998,3]]}},"alternative-id":["4"],"URL":"https:\/\/doi.org\/10.1007\/s003780050012","relation":{},"ISSN":["0945-8115","1432-2188"],"issn-type":[{"value":"0945-8115","type":"print"},{"value":"1432-2188","type":"electronic"}],"subject":[],"published":{"date-parts":[[1998,3]]}}}