proverには担当分野があります．例えば # MESON[] `1+2=1+2`;; 0..0..solved at 2 val it : thm = |- 1 + 2 = 1 + 2 は処理できても # MESON[] `1+2=2+1`;; 0..0..1..2..6..11..19..30..41..54..81..108..149..214..279..368..489..610..763..9 96..1229..15…

現在の定理証明プログラムは ・論理式を入力すれば，自動的に証明してくれる（ものによっては証明も出力する），いわゆる，prover． 例）otter/prover9 http://www.mcs.anl.gov/research/projects/AR/otter/index.html http://www.cs.unm.edu/~mccune/mace4/…

次の定理の証明を考えて見て下さい． 関数ｆ，ｇに対して，ｆ（ｇ（ｘ））＝ｘをみたすｘが唯一つ存在するならば，ｇ（ｆ（ｙ））＝ｙをみたすｙが唯一つ存在する 特に難しい訳ではないにせよ，ｙ＝ｇ（ｘ），そしてｙが異なればｆ（ｙ）も異なることに気付…

ですが，ユーザーの多さを鑑み，Windowsの場合をお話します（コマンドやパッケージによっては外部プログラムやソースの書き換えが必要になりますが，それは逐次述べます）． まず，HOL Lightは，Objective Caml上のプログラムなので http://caml.inria.fr/pu…

突然（でもないかも？）ですが，今回からしばらく，HOL Lightについて少し詳しく書いて行きたいと思います． まず，インストールですが，前回の方法は，手軽とはいえ HOL Light 2.20, built 22 December 2006 on OCaml 3.09.3 という古い安定化バージョンで…

SOS分解は，不等式のみではなく，一般の半代数系の全称命題の証明にも利用できます．今回は，その実装例であるHOL Light上のREAL_SOSのご紹介します． まず，必要なプログラムをダウンロードしましょう．分解にはcsdpが必要なので sudo leafpad /etc/apt/sou…

先に述べたQEの 【２】過程が普通の証明の参考にならない という性質に関連して，今回は一目瞭然の不等式の証明を提供する「SOS分解」をお話します． SOS（sum of squares）分解とは，与えられた多項式を多項式の平方和に分解する「平方完成の親玉」であり，…

まずは，各*proveの違いを確認します．proveは，a,b,cを prove(a+b>=c); The inequality holds. のように１つの３角形の３辺の長さと見な做します．xproveでは xprove(a+b>=c); output a counter-example [1/4, 1/2, 1] The inequality does not hold. xprov…

いわゆる「不等式の証明」がQEの代表的な応用であることは既にお話した通りですが，そこには 【１】パラメトリックシステム向けの汎用ツールでは効率が悪い 【２】過程が普通の証明の参考にならない といった不満もあります．というわけで今回は，何かと重く…

ある事柄を待っていたのですが，もう１０月ですので，別の主題で再起動したいと思います．