HOL Light
The HOL Light theorem prover Written by John Harrison drawing on the work of Mike Gordon Tom Melham Robin Milner Larry Paulson Konrad Slind and many other HOL and LCF researchers HOL Light is a computer program to help users prove interesting mathematical theorems completely formally in higher order logic. It sets a very exacting standard of correctness, but provides a number of automated tools an
Code and resources for "Handbook of Practical Logic and Automated Reasoning"
Code and resources for "Handbook of Practical Logic and Automated Reasoning" The code available on this page was written by John Harrison to accompany his textbook on logic and automated theorem proving, published in March 2009 by Cambridge University Press. For more information about the book, click the picture on the right. As well as the code, this page includes links to other relevant resource
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
処理を実行中です
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
http://www.cl.cam.ac.uk/~jrh13/papers/mizar_times.pdf
