curringは，OCamlの殆ど，HOL Lightの全ての中置き２項演算子に使われていますが，順序対がないわけではなく，OCaml，HOL Light，それぞれにおいて # 1,2;; val it : int * int = (1, 2) # type_of `1,2`;; val it : hol_type = `:num#num` のようになってい…

例えば，OCamlの加法演算子を引数なしで呼ぶと (+);; val it : int -> int -> int = 同じく，HOL Lightの加法の演算子のhol_typeを見ると type_of `(+)`;; val it : hol_type = `:num->num->num` のようと表示されます．これは例えば「x+1」が，x に対して「…

ここまでの段階でもtermはかなり複雑に見えるかも知れませんが，根本的には次の４種に過ぎません． ・Variables （`x:bool`や`n:num`など） ・Constants （`T`や`(~)`など） ・Applications （`~p`のような演算子を変数に作用させて得られるtermの組合せ）こ…

TAUTのような高い自動性をもつ規則関数と同様，HOL Lightには，繊細な推論用の「導入」と「除去」の規則関数があります． まず，２つのtheorem，A |- p，B |- qからtheorem A∪B |- p∧q を得る規則，つまり，∧を導入するのがCONJです． let thp = ASSUME `p:b…

命題論理の定理式（意味論での恒真式）のproverがTAUTであり，任意の定理式を証明してくれます． TAUT`((p==>q)==>p)==>p`;; val it : thm = |- ((p ==> q) ==> p) ==> p 書き忘れていましたが，HOL Lightは普通の数学と同じく，古典論理を採用していますの…

HOL Lightの命題論理は一般的なものであり，命題定数は F (Falsity) T (Truth) 論理記号は ~ (Not) さらに結合の強い順に /\ (And) \/ (Or) ==> (Implies) (Iff) で，同じ結合記号どうしは右結合，formula，および，truth valuesの設定もごく普通のものです…

ここまでの道具だけで，自明でない定理を証明することはやや辛いです．しかし，HOL Lightには，強力な推論規則により自明でない定理を自動的に証明するproverが実装されています． その一つ，ARITH_RULE関数は，自然数（非負整数）の代数的な順序交換と線形…

述語論理のformulaに当たるtermのhol_typeは `x+1 であり `2+2=5`;; val it : term = `2 + 2 = 5` もhol_typeがboolのtermです． これまでの例からも判る通り，HOL Lightは入力されたtermを直ちには評価しません（Mathematicaなら 2+2は4，2+2=5はFalseと返…

ところが subst[`2`,`x`]`x+1`;; Warning: inventing type variables val it : term = `x + 1` のように上手く行きません．このWarningはterm xのhol_type（というOCamlでのtype）が不明ということなので，例えば，num（自然数，非負整数）と明示すれば subs…

termの例を挙げます． `x+1`;; val it : term = `x + 1` `(x)+1`;; val it : term = `x + 1` ` x + ( 1 ) `;; val it : term = `x + 1` これらはいずれも同じtermで，その内部表現は # remove_printer print_qterm;; `x+1`;; val it : term = ... # install_…

前回お話したtoplevel loopにおいてできることの２つ目は，evaluate expressions，つまり，数や文字列の評価でした． 「HOL Lightは，これに加えて，数学的陳述や論理的主張を表す「term」と，証明済みの主張を表す「theorem」を評価するツールの集まりです…

今回からしばらく 『HOL Light Tutorial (for version 2.20)』 http://www.cl.cam.ac.uk/~jrh13/hol-light/tutorial_220.pdf に従って話を進めます．なお，リファレンスはこちら 『The HOL Light System REFERENCE』 (For HOL Light 2.20++ November 2, 2011…

話が前後しますが，HOL Lightの紹介です． 私の学生時代の愛読書に『数学の基礎』（日本評論社）という島内剛一先生の労作があります．これは初等超越関数までを数理論理の手法により構成したもので，現在においても類書のない一冊だと思います． 一方，計算…

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

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

CAD の話が続きましたので，今回は QE のもう一つの基本，Virtual Substitution of Parametric Test Points をお話しましょう． 随分と長い名前というか，説明そのものですが，直訳なら「変数を含む試験点の仮想的代入」といった所でしょうか？ まぁ呼び方は…

今回は，Mathematica の CAD 関数についてのお話ですが，まずは用語の確認から，．．．，R^{n+1}(n≧1)の部分集合 X が Cylindrical であるとは，R^n の部分集合 Y と Y 上で定義された無限大を含めた実数値関数 f,g が存在して X={(x_1,...,x_n,x_{n+1}) ; (…

Maple 10 で登場した ChainTools パッケージに， Maple 14 で追加されたサブパッケージ SemiAlgebraicSetTools の目玉が，以前出力をご覧頂いた CylindricalAlgebraicDecompose です． この関数は，全空間を与えられた有限個の多項式関数の符号を変えない部…

前回紹介した RealRootClassification および RegularChains[ParametricSystemTools][BorderPolynomial], RegularChains[ParametricSystemTools][DiscriminantSequence], RegularChains[SemiAlgebraicSetTools][RealRootIsolate] with method='Discoverer' …

Maple 13 において，RegularChains のサブパッケージ ParametricSystemTools に加わった RealRootClassification 関数 （RegularChains[ParametricSystemTools] - Maple Programming Help）は，その名の通り，多項式で表された不等式制約を許す連立方程式の…

まず，RootFinding は，Isolate 関数のような方程式の数値解計算を主としたパッケージですが，Maple 12 で追加されたサブパッケージ Parametric は，不等式制約を許す連立方程式の open CAD（パラメータ＝自由変数空間の開集合による分解 http://www.sigsam.…

今回は，CAD は一回お休みして，いきなり始まった「 maxima で QE 」シリーズの１をお送りします． 以下では，∀x P(x) や ∃x P(x) (x∈R^N) のような量化子の種類が 1 で，しかも，自由変数を含まない論理式（閉論理式）を扱います． 閉論理式の真偽を判定す…