{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:47:32Z","timestamp":1749124052101},"reference-count":14,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[1995,3,1]],"date-time":"1995-03-01T00:00:00Z","timestamp":794016000000},"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":["Form. Asp. Comput."],"published-print":{"date-parts":[[1995,3]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>An important advantage of using a formal method of developing software is that one can prove that development steps are correct with respect to their specification. Conducting proofs by hand, however, can be time consuming to the extent that designers have to judge whether a proof of a particular obligation is worth conducting. Even if hand proofs are worth conducting, how do we know that they are correct?<\/jats:p>\n          <jats:p>One approach to overcoming this problem is to use an automatic theorem proving system to develop and check our proofs. However, in order to enable present day theorem provers to check proofs, one has to conduct them in much more detail than hand proofs. Carrying out more detailed proofs is of course more time consuming.<\/jats:p>\n          <jats:p>This paper describes the use of proof by analogy in an attempt to reduce the time spent on proofs. We develop and implement a proof follower based on analogy and present an example to illustrate its characteristics. The example shows that even when the follower fails to complete a proof, it can provide a hint that enables the user to complete a proof.<\/jats:p>","DOI":"10.1007\/bf01211605","type":"journal-article","created":{"date-parts":[[2005,2,25]],"date-time":"2005-02-25T19:41:40Z","timestamp":1109360500000},"page":"183-206","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["Proof by analogy in mural"],"prefix":"10.1145","volume":"7","author":[{"given":"Sunil","family":"Vadera","sequence":"first","affiliation":[{"name":"Department of Mathematics and Computer Science, University of Salford, M5 4WT, Salford, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","unstructured":"Buchanan B. G. et al. Constructing an expert system. In F. Hayes-Roth D. A. Waterman and D. B. Lenat editors Building Expert Systems pages 127\u2013167. Addison Wesley 1983."},{"key":"e_1_2_1_2_2_2","unstructured":"Bundy. A. The Computer Modelling of Mathematical Reasoning . Academic Press 1979."},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"crossref","unstructured":"Bundy. A. The use of explicit plans to guide inductive proofs. In R. Lusk and R. Overbeek editors 9th Conference on Automated Deduction pages 111\u2013120. Springer-Verlag 1988.","DOI":"10.1007\/BFb0012826"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"crossref","unstructured":"Gick M. and Holyoak K. J. Analogical problem solving. Cognitive Psychology 12 1980.","DOI":"10.1016\/0010-0285(80)90013-4"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"publisher","DOI":"10.1016\/0004-3702(89)90003-9"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4471-3180-9","volume-title":"mural;A Formal Development Support System","author":"Jones C. B.","year":"1991"},{"key":"e_1_2_1_2_7_2","unstructured":"Jones C. B. Systematic Software Development using VDM. Prentice Hall International second edition 1990."},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"publisher","DOI":"10.1016\/0004-3702(71)90008-7"},{"key":"e_1_2_1_2_9_2","unstructured":"McDermott J. Learning to use analogies. In Proceedings of the International Joint Conference on Artificial Intelligence pages 568\u2013576 Tokyo 1979."},{"key":"e_1_2_1_2_10_2","volume-title":"PhD thesis","author":"Munyer J. C.","year":"1981"},{"key":"e_1_2_1_2_11_2","volume-title":"The Logical Basis for Computer Programming I","author":"Manna Z.","year":"1985"},{"key":"e_1_2_1_2_12_2","unstructured":"Owen S. Analogy for Automated Reasoning . Academic Press 1990."},{"key":"e_1_2_1_2_13_2","volume-title":"PhD thesis","author":"Vadera S.","year":"1992"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/BF01211605","article-title":"Proof by analogy in mural \u2014 a more detailed account","volume":"7","author":"Vadera S.","year":"1995","journal-title":"Formal Aspects of Computing"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01211605.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF01211605\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/BF01211605","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:22:03Z","timestamp":1641482523000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/BF01211605"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995,3]]},"references-count":14,"journal-issue":{"issue":"2","published-print":{"date-parts":[[1995,3]]}},"alternative-id":["10.1007\/BF01211605"],"URL":"https:\/\/doi.org\/10.1007\/bf01211605","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[1995,3]]}}}