http://cstheory.blogoverflow.com/2012/02/something-you-should-know-about-quantifier-elimination-part-ii/ の間違いを http://math.umh.ac.be/preprints/src/Ozturk020411.pdf に従って修正して、自由変数がある場合の量化子除去もできるようになった。
試しに ∃x. a^2*x + b*x + c = 0 の量化子除去をしてみるとこんな感じ。
(a = 0 ∧ 2*a = 0 ∧ b = 0 ∧ c = 0) ∨
(a = 0 ∧ 2*a = 0 ∧ b < 0) ∨
(a = 0 ∧ 2*a = 0 ∧ b > 0) ∨
(a = 0 ∧ 2*a < 0 ∧ 2*a*c - b^2 < 0 ∧ b < 0) ∨
(a = 0 ∧ 2*a < 0 ∧ 2*a*c - b^2 = 0 ∧ b < 0) ∨
(a = 0 ∧ 2*a < 0 ∧ 2*a*c - b^2 > 0 ∧ b < 0) ∨
(a = 0 ∧ 2*a < 0 ∧ 2*a*c - b^2 < 0 ∧ b > 0) ∨
(a = 0 ∧ 2*a < 0 ∧ 2*a*c - b^2 = 0 ∧ b > 0) ∨
(a = 0 ∧ 2*a < 0 ∧ 2*a*c - b^2 > 0 ∧ b > 0) ∨
(a = 0 ∧ 2*a > 0 ∧ 2*a*c - b^2 < 0 ∧ b < 0) ∨
(a = 0 ∧ 2*a > 0 ∧ 2*a*c - b^2 = 0 ∧ b < 0) ∨
(a = 0 ∧ 2*a > 0 ∧ 2*a*c - b^2 > 0 ∧ b < 0) ∨
(a = 0 ∧ 2*a > 0 ∧ 2*a*c - b^2 < 0 ∧ b > 0) ∨
(a = 0 ∧ 2*a > 0 ∧ 2*a*c - b^2 = 0 ∧ b > 0) ∨
(a = 0 ∧ 2*a > 0 ∧ 2*a*c - b^2 > 0 ∧ b > 0) ∨
(a < 0 ∧ 2*a < 0 ∧ 4*a^2*c - a*b^2 = 0) ∨
(a < 0 ∧ 2*a < 0 ∧ 4*a^2*c - a*b^2 > 0) ∨
(a > 0 ∧ 2*a < 0 ∧ 4*a^2*c - a*b^2 < 0) ∨
(a > 0 ∧ 2*a < 0 ∧ 4*a^2*c - a*b^2 = 0) ∨
(a < 0 ∧ 2*a > 0 ∧ 4*a^2*c - a*b^2 = 0) ∨
(a < 0 ∧ 2*a > 0 ∧ 4*a^2*c - a*b^2 > 0) ∨
(a > 0 ∧ 2*a > 0 ∧ 4*a^2*c - a*b^2 < 0) ∨
(a > 0 ∧ 2*a > 0 ∧ 4*a^2*c - a*b^2 = 0)
条件の不整合性とかを全然検査していないので、余計なものも沢山出てきている。余計なやつを手で消してみるとこんな感じか。
(a = 0 ∧ 2*a = 0 ∧ b = 0 ∧ c = 0) ∨
(a = 0 ∧ 2*a = 0 ∧ b < 0) ∨
(a = 0 ∧ 2*a = 0 ∧ b > 0) ∨
(a < 0 ∧ 2*a < 0 ∧ 4*a^2*c - a*b^2 = 0) ∨
(a < 0 ∧ 2*a < 0 ∧ 4*a^2*c - a*b^2 > 0) ∨
(a > 0 ∧ 2*a > 0 ∧ 4*a^2*c - a*b^2 < 0) ∨
(a > 0 ∧ 2*a > 0 ∧ 4*a^2*c - a*b^2 = 0)
だいぶマシだけれど、でも b^2 - 4ac ≧ 0 が簡単に出てくるわけではないのね……