2013-02-23から1日間の記事一覧
関数 g で始まる HOL Light の対話的証明作成では,論理式 ~(A0) ∨ … ∨ ~(An) ∨ B が定理式であること,つまり [A0] … [An] A0,..,An |- B あるいは B を 0 [A0] ……… n [An] B と表示します.・HOL Light のプルーフマネージャーは証明を遡って作成しますの…
関数 g で始まる HOL Light の対話的証明作成では,論理式 ~(A0) ∨ … ∨ ~(An) ∨ B が定理式であること,つまり [A0] … [An] A0,..,An |- B あるいは B を 0 [A0] ……… n [An] B と表示します.・HOL Light のプルーフマネージャーは証明を遡って作成しますの…