MINLOG: Difference between revisions
m subst |
m damnit |
||
| Line 1: | Line 1: | ||
{{ |
{{dated prod|concern = {{{concern|fails to assert notability}}}|month = July|day = 10|year = 2007|time = 09:18|timestamp = 20070710091840}} |
||
<!-- Do not use the "dated prod" template directly; the above line is generated by "subst:prod|reason" --> |
|||
'''MINLOG''' is a [[proof assistant]] developed at the University of Munich by the team of [[Helmut Schwichtenberg]]. |
'''MINLOG''' is a [[proof assistant]] developed at the University of Munich by the team of [[Helmut Schwichtenberg]]. |
||
Revision as of 09:18, 10 July 2007
It is proposed that this article be deleted because of the following concern:
If you can address this concern by improving, copyediting, sourcing, renaming, or merging the page, please edit this page and do so. You may remove this message if you improve the article or otherwise object to deletion for any reason. Although not required, you are encouraged to explain why you object to the deletion, either in your edit summary or on the talk page. If this template is removed, do not replace it. This message has remained in place for seven days, so the article may be deleted without further notice. Find sources: "MINLOG" – news · newspapers · books · scholar · JSTOR Nominator: Please consider notifying the author/project: {{subst:proposed deletion notify|MINLOG|concern=fails to assert notability}} ~~~~Timestamp: 20070710091840 09:18, 10 July 2007 (UTC) Administrators: delete |
MINLOG is a proof assistant developed at the University of Munich by the team of Helmut Schwichtenberg.
MINLOG is based on first order natural deduction calculus. It is intended to reason about computable functionals, using minimal rather than classical or intuitionistic logic. The main motivation behind MINLOG is to exploit the proofs-as-programs paradigm for program development and program verification. Proofs are in fact treated as first class objects which can be normalized. If a formula is existential then its proof can be used for reading off an instance of it, or changed appropriately for program development by proof transformation. To this end MINLOG is equipped with tools to extract functional programs directly from proof terms. This also applies to non-constructive proofs, using a refined A-translation. The system is supported by automatic proof search and normalization by evaluation as an efficient term rewriting device.