2013-03-14から1日間の記事一覧

不等式の性質 by HOL4.

http://d.hatena.ne.jp/ehito/20130313/1363131870 の定理の HOL4 による証明です. - g `!s t a b:real. 0<=s /\ 0<=t /\ (s+t=1) /\ 0<=a /\ 0<=b ==> !n. (s*a+t*b) pow n <= s*a pow n + t*b pow n` ; > val it = Proof manager status: 1 proof. 1. Inc…

形式化された定理の証明では...

適当な tactics を用いて論理記号を外し,atomic formula に分解する作業にそれほどの困難はありません.問題は,そのあと,定数,変数,関数,述語記号などからなる式を「計算」により証明する部分にあります.実際,各種の「検証」で高名な HOL4 も他の証…