Web上の例題

　既出の本家筋以外は中々見当たらないのですが，次の論文の補足Ｂに入門的な解説があります．
http://rudar.ruc.dk/bitstream/1800/6890/1/8%20-%20Automatization%20of%20the%20semantic%20tableau%20method.pdf

　なお，取り上げられている例をただ証明するだけなら

# let t = `!n. ODD (3 * n + 2) ==> ODD n` ;;
val t : term = `!n. ODD (3 * n + 2) ==> ODD n`
# MESON[ODD_ADD; ODD_MULT; ARITH_RULE `~ODD 2`] t;;
0..0..2..8..33..solved at 47
val it : thm = |- !n. ODD (3 * n + 2) ==> ODD n
# MESON[NOT_ODD; EVEN_ADD; EVEN_MULT; ARITH_RULE `EVEN 2`] t;;
0..0..1..5..14..43..146..solved at 189
val it : thm = |- !n. ODD (3 * n + 2) ==> ODD n

あるいは，MESONの検索が長くなりますが，ARITH_RULE を用いずに

# MESON[NOT_ODD; EVEN_ADD; EVEN_MULT; EVEN_DOUBLE; MULT_CLAUSES] t;;
0..0..1..5..18..65..239..803..3025..solved at 3624
val it : thm = |- !n. ODD (3 * n + 2) ==> ODD n
# MESON [ODD_ADD; ODD_MULT; ONE; TWO; ODD] t;;
0..0..2..11..53..234..1104..5615..28515..155554..898058..5273951..solved at 11076498
val it : thm = |- !n. ODD (3 * n + 2) ==> ODD n

または，手続きを追って

prove
 (`!n. ODD (3 * n + 2) ==> ODD n`,
  GEN_TAC THEN CONV_TAC CONTRAPOS_CONV THEN 
  SIMP_TAC[NOT_ODD; EVEN_EXISTS] THEN STRIP_TAC THEN ASM_SIMP_TAC[] THEN 
  EXISTS_TAC `3 * m + 1` THEN ARITH_TAC);;

等とするのが簡明です．