ここまでの段階でも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_…