Difference between revisions of "OpenProofPower"
(Created page with "{{Entry |Name=OpenProofPower |Short description=a specification and proof tool |Full description=OpenProofPower is a specification and proof tool based on an implementation of Hi...") |
(New version) |
||
Line 3: | Line 3: | ||
|Short description=a specification and proof tool | |Short description=a specification and proof tool | ||
|Full description=OpenProofPower is a specification and proof tool based on an implementation of Higher Order Logic (HOL), following the LCF paradigm, in Standard ML. OpenProofPower provides support for specification and proof in Z using a semantic embedding of Z into HOL. | |Full description=OpenProofPower is a specification and proof tool based on an implementation of Higher Order Logic (HOL), following the LCF paradigm, in Standard ML. OpenProofPower provides support for specification and proof in Z using a semantic embedding of Z into HOL. | ||
+ | |Homepage URL=http://www.lemma-one.com/ProofPower/index | ||
|User level=intermediate | |User level=intermediate | ||
− | |||
− | |||
− | |||
− | |||
|Computer languages=ml | |Computer languages=ml | ||
− | |||
− | |||
− | |||
− | |||
− | |||
|Related projects=The_Jaza_Animator | |Related projects=The_Jaza_Animator | ||
|Keywords=Z,specification,formal methods,formal,HOL,Higher Order Logic,Z notation | |Keywords=Z,specification,formal methods,formal,HOL,Higher Order Logic,Z notation | ||
− | | | + | |Version identifier=3.1w7 |
− | |Last review by= | + | |Version date=2016/03/13 |
− | |Last review date= | + | |Version status=stable |
+ | |Version download=http://www.lemma-one.com/ProofPower/getting/versions/OpenProofPower-3.1w7.tgz | ||
+ | |Last review by=Alejandroindependiente | ||
+ | |Last review date=2017/01/19 | ||
|Submitted by=Database conversion | |Submitted by=Database conversion | ||
|Submitted date=2011-04-01 | |Submitted date=2011-04-01 | ||
− | | | + | |Status= |
− | | | + | |Is GNU=No |
− | | | + | |License verified date=2008-06-23 |
− | | | + | }} |
+ | {{Project license | ||
+ | |License=GPLv2 | ||
+ | |License verified by=Deborah Nicholson | ||
|License verified date=2008-06-23 | |License verified date=2008-06-23 | ||
− | |||
}} | }} | ||
{{Person | {{Person | ||
+ | |Real name=Rob Arthan | ||
|Role=Developer | |Role=Developer | ||
− | + | |Resource URL= | |
− | |||
− | |Resource URL= | ||
}} | }} | ||
{{Software category | {{Software category | ||
Line 39: | Line 35: | ||
|Use=software-development | |Use=software-development | ||
}} | }} | ||
− | {{ | + | {{Featured}} |
− | |||
− | |||
− | |||
− | }} |
Latest revision as of 16:02, 19 January 2017
OpenProofPower
http://www.lemma-one.com/ProofPower/index
a specification and proof tool
OpenProofPower is a specification and proof tool based on an implementation of Higher Order Logic (HOL), following the LCF paradigm, in Standard ML. OpenProofPower provides support for specification and proof in Z using a semantic embedding of Z into HOL.
Licensing
License
Verified by
Verified on
Notes
Leaders and contributors
Contact(s) | Role |
---|---|
Rob Arthan | Developer |
Resources and communication
Software prerequisites
Permission is granted to copy, distribute and/or modify this document under the terms of the GNU Free Documentation License, Version 1.3 or any later version published by the Free Software Foundation; with no Invariant Sections, no Front-Cover Texts, and no Back-Cover Texts. A copy of the license is included in the page “GNU Free Documentation License”.
The copyright and license notices on this page only apply to the text on this page. Any software or copyright-licenses or other similar notices described in this text has its own copyright notice and license, which can usually be found in the distribution or license text itself.