Loading article…
数理論理学において、実数の1階言語とは、全称量化子と存在量化子、および実変数に関する式の等号と不等号の論理的組み合わせを含む、 1階論理のすべての整形式文の集合である。対応する1階理論とは、実際に実数について真となる文の集合である。このような理論はいくつかあり、表現力は、式で使用できる基本演算によって異なる。これらの理論の研究における根本的な問題は、それらが決定可能であるかどうか、つまり、文を入力として受け取り、その文が理論において真であるかどうかという問いに対して「はい」または「いいえ」という答えを出力として生成できるアルゴリズムが存在するかどうかである。
実閉体理論とは、基本演算が乗算と加算である理論のことです。つまり、この理論では、定義できる数は実代数的数に限られます。タルスキによって証明されたように、この理論は決定可能です（タルスキ・ザイデンベルクの定理および量化子消去を参照）。実閉体理論の決定手続きの現在の実装は、円筒代数分解による量化子消去に基づいていることが多いです。
タルスキーの決定可能なアルゴリズムは1950年代に電子計算機に実装されました。実行時間が遅すぎるため、興味深い結果を得ることはできません。[ 1 ]
タルスキーの指数関数問題は、この理論を別の原始演算である指数関数に拡張することに関するものです。この理論が決定可能かどうかは未解決の問題ですが、シャヌエルの予想が成り立つならば、この理論の決定可能性が導かれるでしょう。[ 2 ] [ 3 ]対照的に、正弦関数による実閉体の理論の拡張は、決定不可能な整数の理論を符号化できるため、決定不可能です（リチャードソンの定理を参照）。
それでも、正弦関数などの決定不能なケースは、必ずしも常に終了するとは限らないアルゴリズムを使用することで対処できます。特に、入力式が頑健である、つまり、式がわずかに摂動されても充足可能性が変わらない式に対してのみ終了する必要があるアルゴリズムを設計できます。[ 4 ]あるいは、純粋にヒューリスティックなアプローチを使用することもできます。[ 5 ]