9.3 Quantifier elimination

　今回は，特称量化にも対応した一般の半代数系の prover についてです．

■　まず，:num，:intにおける線形系のそれは

#use "Examples/cooper.ml";;

とロードして使う，Cooperのアルゴリズムに基づく関数，COOPER_RULE，INT_COOPERです．

# ARITH_RULE `?x. 0=x`;;
Exception: Failure "linear_ineqs: no contradiction".
# COOPER_RULE `?x. 0=x`;;
val it : thm = |- ?x. 0 = x
# COOPER_RULE `ODD n ==> 2 * n DIV 2 < n`;;
val it : thm = |- ODD n ==> 2 * n DIV 2 < n
# COOPER_RULE `!n. n >= 8 ==> ?a b. n = 3 * a + 5 * b`;;
val it : thm = |- !n. n >= 8 ==> (?a b. n = 3 * a + 5 * b)
# INT_COOPER `!n. ?a. n= &3*a \/ n= &3*a+ &1 \/ n= &3*a+ &2`;;
val it : thm = |- !n. ?a. n = &3 * a \/ n = &3 * a + &1 \/ n = &3 * a + &2

　この２つのproversは:int上の Quantifier Elimination conversion，COOPER_CONV を内部で呼んでいます．

# COOPER_CONV `?a. n= &3*a`;;
val it : thm = |- (?a. n = &3 * a) <=> -- &3 divides -- &1 * n

# COOPER_CONV `!x. a<=x==>b b < x) <=> &0 < a + -- &1 * b

# COOPER_CONV `!x. ~(?m. x = &2 * m) /\ (?m. x = &3 * m + &1) <=>
(?m. x = &12 * m + &1) \/ (?m. x = &12 * m + &7)`;;
val it : thm =
|- (!x. ~(?m. x = &2 * m) /\ (?m. x = &3 * m + &1) <=>
(?m. x = &12 * m + &1) \/ (?m. x = &12 * m + &7)) <=>
T

　ただし，Cooperのアルゴリズムでは，非線形の半代数系は扱えません．

# COOPER_CONV `?x. &0 = x`;;
val it : thm = |- (?x. &0 = x) <=> T

# COOPER_CONV `?x. &0 = x * x`;;
Exception: Failure "PART_MATCH: Sanity check failure".

■　一方，:real 上には，非線形システムも評価できる QE conversion，REAL_QELIM_CONV ( http://www.cs.cmu.edu/~seanmcl/papers/McLaughlin-CADE-2005.pdf ) があり

#use "Rqe/make.ml";;

とロードすれば使えます．

# REAL_QELIM_CONV `!a. ~(a= &0) ==> ?x. &1=a*x` ;;
val it : thm = |- (!a. ~(a = &0) ==> (?x'. &1 = a * x')) <=> T

# REAL_QELIM_CONV `!a b. a<b ==> ?x. a<x /\ x<b` ;;
val it : thm = |- (!a b. a < b ==> (?x'. a < x' /\ x' < b)) <=> T

# REAL_QELIM_CONV `?x. x pow 2 = a /\ !y. y pow 2 = a ==> y=x`;;
val it : thm =
  |- (?x. x pow 2 = a /\ (!y. y pow 2 = a ==> y = x)) <=> &0 + a * -- &2 = &0

# REAL_QELIM_CONV `?x. x pow 3 = a`;;
val it : thm =
  |- (?x. x pow 3 = a) <=>
     &0 + a * -- &3 = &0 \/
     ~(&0 + a * -- &3 = &0) /\ (&0 + a * -- &3 > &0 \/ &0 + a * -- &3 < &0)

# REAL_QELIM_CONV `?x. x pow 4 = a`;;
val it : thm =
  |- (?x. x pow 4 = a) <=>
     &0 + a * -- &4 = &0 \/ ~(&0 + a * -- &4 = &0) /\ &0 + a * -- &4 < &0

# REAL_QELIM_CONV `!k. (?x. x pow 3 - &3*x + k < &0 /\ &0 < x) <=> k < &2` ;;
val it : thm =
  |- (!k. (?x'. x' pow 3 - &3 * x' + k < &0 /\ &0 < x') <=> k < &2) <=> T

# REAL_QELIM_CONV `!x y e h. &0 < e ==> ?d. &0 < d /\ -- d < h /\ h < d ==> (x + h) * (y + h) -
x * y < e /\ x * y - (x + h) * (y + h) < e`;;
val it : thm =
  |- (!x y e h.
          &0 < e
          ==> (?d. &0 < d /\ --d < h /\ h < d
                   ==> (x + h) * (y + h) - x * y < e /\
                       x * y - (x + h) * (y + h) < e)) <=>
     T

　ただし，処理速度は，CADやVSベースのReduce on Mathematica，rlqe on REDUCE，QEPCADなどとは比較になりません．
http://www.philipp.ruemmer.org/publications/rwv.pdf