“Parametric Robust Control by Quantifier Elimination” http://www.jssac.info/Editor/Suushiki/V10/No1/V10N1_106.pdf に載っていた以下のような非常に素朴な virtual substitution を以前に実装した https://github.com/msakai/toysolver/blob/c853c4610f3cee09f8bca4205294463c4071cae7/src/ToySolver/Arith/VirtualSubstitution.hs 。
(∃x. φ(x)) ⇔ ∨_{t∈S} φ(t)
WHERE
{a_i x - b_i ρ_i 0 | i ∈ I, ρ_i ∈ {=, ≠, ≤, <}} is the set of atomic subformulas in φ(x)
S = { b_i / a_i, b_i / a_i + 1, b_i / a_i - 1 | i∈I } ∪ {1/2 (b_i / a_i + b_j / a_j) | i,j∈I, i≠j}
この elimination set S は流石に無駄な要素が多く含まれていて、試してみると実際効率が悪い。“Applying linear quantifier elimination”(R. Loos and V. Weispfenning)にはより効率的な方法が載っているそうだが、とりあえず自分で(Cooperのアルゴリズムを参考に)より効率的な elimination set を考えてみると、=,≠の除去、否定標準形への変換を行っておいて、
{ -∞ } ∪ L1 ∪ { (l+u)/2 | l∈L2, u∈U } ∪ { l+1 | l∈L2 }
WHERE
L1 = { l | (l≤x) は φ(x) 中の原子論理式の変形, x∉FV(l) }
L2 = { l | (l<x) は φ(x) 中の原子論理式の変形, x∉FV(l) }
U = { u | (x≤u) もしくは (x<u) は φ(x) 中の原子論理式の変形, x∉FV(u) }
としてはどうだろうか。ただし、φ(-∞) はφ(x)中の、x≤t,x<tを真に、t≤x,t<xを偽に、それぞれ置き換えた論理式とする。