Prof Sunil Vadera S.Vadera@salford.ac.uk
Professor
Proof by analogy in mural
Vadera, S
Authors
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.
Citation
Vadera, S. (1995). Proof by analogy in mural. Formal Aspects of Computing, 7(2), 183-206. https://doi.org/10.1007/BF01211605
Journal Article Type | Article |
---|---|
Publication Date | Jan 1, 1995 |
Deposit Date | Jun 23, 2010 |
Publicly Available Date | Apr 5, 2016 |
Journal | Formal Aspects of Computing |
Print ISSN | 0934-5043 |
Publisher | Springer Verlag |
Peer Reviewed | Peer Reviewed |
Volume | 7 |
Issue | 2 |
Pages | 183-206 |
DOI | https://doi.org/10.1007/BF01211605 |
Keywords | Formal Methods, VDM, Analogy |
Publisher URL | http://dx.doi.org/10.1007/BF01211605 |
Files
Accepted Version
(407 Kb)
PDF
You might also like
Development of an evolutionary cost sensitive decision tree induction algorithm
(2022)
Presentation / Conference
Phishing website detection from URLs using classical machine learning ANN model
(2021)
Journal Article
Cost-sensitive meta-learning framework
(2021)
Journal Article
Phishing email detection using Natural Language Processing techniques : a literature survey
(2021)
Journal Article
Downloadable Citations
About USIR
Administrator e-mail: library-research@salford.ac.uk
This application uses the following open-source libraries:
SheetJS Community Edition
Apache License Version 2.0 (http://www.apache.org/licenses/)
PDF.js
Apache License Version 2.0 (http://www.apache.org/licenses/)
Font Awesome
SIL OFL 1.1 (http://scripts.sil.org/OFL)
MIT License (http://opensource.org/licenses/mit-license.html)
CC BY 3.0 ( http://creativecommons.org/licenses/by/3.0/)
Powered by Worktribe © 2024
Advanced Search