2013-03-11から1日間の記事一覧
やはり METIS は優秀です. http://www.gilith.com/research/metis/ MESON による PROVE_TAC ではこうは行きません. load "numRingLib"; open arithmeticTheory numLib numRingLib; val def1 = Define `p n = (n*n+n+1) MOD 5 <> 0`; val def2 = Define `p0…
やはり METIS は優秀です. http://www.gilith.com/research/metis/ MESON による PROVE_TAC ではこうは行きません. load "numRingLib"; open arithmeticTheory numLib numRingLib; val def1 = Define `p n = (n*n+n+1) MOD 5 <> 0`; val def2 = Define `p0…