Skip to the content

Proof by analogy in mural

Vadera, S 1995, 'Proof by analogy in mural' , Formal Aspects of Computing, 7 (2) , pp. 183-206.

[img]
Preview
PDF - Accepted Version
Download (397kB) | Preview

    Abstract

    One of the most important advantages 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? 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. 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 two examples to illustrate its characteristics. One example illustrates the successful use of the proof follower. The other example illustrates that the follower's failure can provide a hint that enables the user to complete a proof.

    Item Type: Article
    Uncontrolled Keywords: Formal Methods, VDM, Analogy
    Themes: Subjects / Themes > Q Science > QA Mathematics > QA075 Electronic computers. Computer science
    Subjects outside of the University Themes
    Schools: Colleges and Schools > College of Science & Technology
    Colleges and Schools > College of Science & Technology > School of Computing, Science and Engineering
    Colleges and Schools > College of Science & Technology > School of Computing, Science and Engineering > Data Mining and Pattern Recognition Research Centre
    Journal or Publication Title: Formal Aspects of Computing
    Publisher: Springer Verlag
    Refereed: Yes
    ISSN: 0934-5043
    Depositing User: S Vadera
    Date Deposited: 23 Jun 2010 11:03
    Last Modified: 20 Aug 2013 17:19
    URI: http://usir.salford.ac.uk/id/eprint/9401

    Document Downloads

    More statistics for this item...

    Actions (login required)

    Edit record (repository staff only)