空中戦
\( \forall x \)や\( \exists y\)などの量限定子がついた変数を全て除去出来れば、自由変数だけからなる式が出来ます。これを同値変形で求めることができれば、量限定子除去した結果の自由変数の式は元の式が成立するための（必要十分）条件となります。
変数の領域を実数にとり、多変数多項式を項として、等号、不等号を述語とする１階述語論理では、量限定子除去(Q.E.)をすることが可能で、そのためのアルゴリズムがあります。よく知られているアルゴリズムはCylindrical Algebraic Decomposition (略してCAD)とかVirtual Substitutionなどです。
Q.E.を日本語で勉強するために、非常に良い本が出ています。
この本には量限定子除去について、基本的なこと、例題、CADなどのアルゴリズム、応用などが書かれています。とても参考になる良い本です。
この本にも紹介されていますが、多くの数式処理システムにはなにかの形で量限定子除去が組み込まれています。Mathematica, Maple, Reduceにはそのためのコマンドがあります。Mathematicaには最初から組み込まれていますし、Maple, Reduceでは拡張コマンドとして提供されています。またQ.E.を行うための専用数式処理プログラムもあります。Qepcad BはQ.E.だけを行えるソフトウェアです。
ではMaximaの状況は、、、どうでしょうか。実はMaximaにはQ.E.は実装されていませんでした。また拡張パッケージとして提供されてもいませんでした。つまり全くQ.E.とは無縁だったと思います。
でもQ.E.って面白そうですよね。大学入試問題のややこしいやつは大抵Q.E.で解けます。多項式関数の最大最小、円と直線の関係、線形計画法やその一部に非線形項が入った場合、、、変数が少なく、次数が低ければ様々な問題を解くことができます。
そこで、、、Maximaから専用プログラムQepcad Bを呼び出す拡張パッケージ、Qepmaxを作ってみました。Maximaで一階述語論理の式を書いて、qe()というコマンドに渡します。内部的にはQepcad Bを呼び出してQ.E.を実行します。qe()はその結果を読み込んでMaximaの式に変換します。
次回からはQepcad B + Qepmaxを使い、MaximaでQ.E.が実行出来る様子をお見せします。
