6.2 First-order reasoning
量化子のネストにおいて変数の依存関係に注意が必要であることは，連続と一様連続との違いを持ち出すまでもなく，明らかでしょう．
さて，先に述べたトートロジーprover TAUTでは，自明でない量化された式の評価はできません，HOL Light には，model elimination (Loveland 1968;
Stickel 1988)と呼ばれる証明検索方法を用いたprover MESON によりtheoremを評価することができます．（通常，theoremでないことを示す代わり，無限ループになったり，有限の深さで処理を終了します．）
古典的な「三段論法」をMESONで証明して見ましょう．
MESON[] `(!x. man(x) ==> mortal(x)) /\ man(Socrates) ==> mortal(Socrates)`;;
Warning: inventing type variables
0..0..1..solved at 4
val it : thm =
|- (!x. man x ==> mortal x) /\ man Socrates ==> mortal Socrates
MESONは，高度に自動化された非常に手軽なツールであり，次のようなストレートな推論においてはそのことが顕著です．
MESON[]
`( (?x. !y. P(x) <=> P(y)) <=> ( (?x. Q(x)) <=> (!y. Q(y)))) <=>
( (?x. !y. Q(x) <=> Q(y)) <=> ( (?x. P(x)) <=> (!y. P(y))))`;;
...
val it : thm =
|- ( (?x. !y. P x <=> P y) <=> (?x. Q x) <=> (!y. Q y)) <=>
(?x. !y. Q x <=> Q y) <=>
(?x. P x) <=>
(!y. P y)
それは時に人間より遥かに高速です．
# MESON[]
`(!x y z. P x y /\ P y z ==> P x z) /\
(!x y z. Q x y /\ Q y z ==> Q x z) /\
(!x y. P x y ==> P y x) /\
(!x y. P x y \/ Q x y)
==> (!x y. P x y) \/ (!x y. Q x y)`;;
Warning: inventing type variables
0..0..2..7..16..30..48..72..108..168..236..340..516..702..918..1260..1660..2098.
.2716..3438..4298..5528..6944..8594..11052..13780..16742..20862..solved at 23107val it : thm =
|- (!x y z. P x y /\ P y z ==> P x z) /\
(!x y z. Q x y /\ Q y z ==> Q x z) /\
(!x y. P x y ==> P y x) /\
(!x y. P x y \/ Q x y)
==> (!x y. P x y) \/ (!x y. Q x y)
しかし，MESONが知ってるのは等号理論までなので
# MESON `1+1=2` ;;
0..0..1..2..5..9..15..24..33..44..64..84..113..158..203..264..348..432..539..698
..857..1068..1328..1588..1897..2295..2693..3180..3835..4490..5313..6322..7331..8
526..10070..11614..13507..16006..18505..21610..25483..29356..33997..40088..46179
..53720..63878..74036..86811..103236..119661..Exception: Failure "solve_goal: To
o deep".
# MESON `!x:num.x>=0` ;;
0..0..1..2..3..4..5..6..7..8..9..10..11..12..13..14..15..16..17..18..19..20..21.
.22..23..24..25..26..27..28..29..30..31..32..33..34..35..36..37..38..39..40..41.
.42..43..44..45..46..47..48..49..Exception: Failure "solve_goal: Too deep".
のようになります．ところが，次は証明できます．
# MESON[]
`(!x. x <= x) /\
(!x y z. x <= y /\ y <= z ==> x <= z) /\
(!x y. f(x) <= y <=> x <= g(y))
==> (!x y. x <= y ==> f(x) <= f(y)) /\
(!x y. x <= y ==> g(x) <= g(y))`;;
0..0..1..3..7..15..solved at 21
0..0..1..3..7..14..solved at 21
val it : thm =
|- (!x. x <= x) /\
(!x y z. x <= y /\ y <= z ==> x <= z) /\
(!x y. f x <= y <=> x <= g y)
==> (!x y. x <= y ==> f x <= f y) /\ (!x y. x <= y ==> g x <= g y)
これは不等式の性質をその場で与えたからであり，所謂，不等式でなくても，証明に用いる反射，対称，推移律を満たす2項関係ならよいので
# MESON[]
`(!x. R x x) /\
(!x y z. R x y /\ R y z ==> R x z) /\
(!x y. R (f x) y <=> R x (g y))
==> (!x y. R x y ==> R (f x) (f y)) /\
(!x y. R x y ==> R (g x) (g y))`;;
Warning: inventing type variables
0..0..1..3..7..15..solved at 21
0..0..1..3..7..14..solved at 21
val it : thm =
|- (!x. R x x) /\
(!x y z. R x y /\ R y z ==> R x z) /\
(!x y. R (f x) y <=> R x (g y))
==> (!x y. R x y ==> R (f x) (f y)) /\ (!x y. R x y ==> R (g x) (g y))
のように証明できます．
また，一意的存在量化子も
MESON[] `(?!x. g(f x) = x) <=> (?!y. f(g y) = y)`;;
Warning: inventing type variables
0..0..1..solved at 4
0..0..1..2..6..12..25..46..82..142..238..390..solved at 431
0..0..1..solved at 4
0..0..1..2..6..12..25..46..82..142..238..390..solved at 431
val it : thm = |- (?!x. g (f x) = x) <=> (?!y. f (g y) = y)
のように扱えます．
そしてMESONを引数なしで呼ぶと
# MESON;;
val it : thm list -> term -> thm =
なので，第一引数を空リスト[ ]ではなく，証明に必要なtheoremsのリストを与えると
# MESON [ADD_ASSOC; ADD_SYM] `m + (n + p) = n + (m + p)`;;
0..0..1..2..7..14..35..62..solved at 73
val it : thm = |- m + n + p = n + m + p
のように評価してくれます．
