次に全称量化をとるまえの状態に戻します． e( GEN_TAC );; すると val it : goalstack = 1 subgoal (1 total) `m = 0 \/ 3 EXP m MOD 3 = 0` のように !m. が付かないものが改めて目標（サブゴール）となります．さて，この式を証明するには，明らかにmが0…

では証明を書いていきましょう．簡単過ぎるのもおもしろくないので 任意の自然数 m に対して m=0 または 3^mを3で割った余りが0 の証明からはじめます．まずこれを論理式に直して，目標（ゴール）に設定します． g `!m. m = 0 \/ 3 EXP m MOD 3 = 0`;; g と…

先ほどの hol_light フォルダーにおいて， rlwrap -r ocaml と入力すると Objective Caml version 3.11.2 # のようにOCamelのインタープリタが起動するので，プロンプトに #use"hol.ml";; と（ # 記号も）入力，しばし待てば Camlp5 Parsing version 5.14 # …

新年度ということで，従来の内容に加え，これから HOL Light を始める方に向けた記事も書いていきます．プラットフォームは，Linux（MS-Windowsの方は http://d.hatena.ne.jp/ehito/20110203/1296713729 を参考にしてください）とします．まず，ターミナルを…