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

ところが．．．

HOL Light には Prover9 という頼もしい友がいます． # #use "Examples/prover9.ml" ;; val prover9 : string = "prover9" val prover9_debugging : bool ref = {contents = false} val prover9_options : string ref = {contents = "clear(auto_inference).…

それでも HOL4 には．．．

METIS があります．HOL Light には MESON しかなく，口惜しい限りです． load "dividesTheory"; open dividesTheory; val ARITH_RULE = SIMP_CONV(arith_ss++ARITH_ss)[divides_def]; val lem = ARITH_RULE ``~(9=0:num) /\ ~(2=0:num) /\ ~(4=0:num) /\ ~(5…