論理関数処理による論理式の簡単化-包括的グレブナ一基底系を利用した限量記号消去編一

摘要

限量記号消去法(Quantifier Elimination: QE)は限量記号がついた一階述語論理式を入力として, それと等価で限量記号のない論理式を出力するアルゴリズムである.例えば,ヨx(x~2+ bx + c = 0) に対してQEを適用すると,それと等価で限量記号がついた変数хのない論理式b~2-4c ≥ 0を得る.一階述語論理式は,限量記号であるV (全称記号),ヨ(存在記号),多項式の等式?不等式からなる原子論理式,Λ (かつ)?v (または)(否定)などの論理演算子から成る.