Entscheidungsproblem

数学とコンピュータ科学において、決定問題（ドイツ語で「決定問題」、発音は[ ɛntˈʃaɪ̯dʊŋspʁoˌbleːm ] ）は、1928年にデイヴィッド・ヒルベルトとヴィルヘルム・アッカーマンによって提起された課題である。^{[ 1 ]}これは、入力された文を考慮し、それが普遍的に妥当であるかどうか、つまりあらゆる構造に​​おいて妥当であるかどうかに応じて「はい」または「いいえ」と答えるアルゴリズムを要求するものである。このようなアルゴリズムは、1936年にアロンゾ・チャーチとアラン・チューリングによって不可能であることが証明された。

一階述語論理の完全性定理によれば、命題は論理規則と公理を用いて推論できる場合に限り普遍的に妥当である。したがって、決定問題は、与えられた命題が論理規則を用いて証明可能かどうかを判断するアルゴリズムを求める問題と見なすこともできる。

1936年、アロンゾ・チャーチとアラン・チューリングはそれぞれ独立した論文^{[ 2 ]}を発表し、「実質的に計算可能」という直感的な概念がチューリングマシンで計算可能な関数（あるいは同等に、ラムダ計算で表現可能な関数）によって捉えられると仮定すると、決定問題の一般的な解は不可能であることを示した。この仮定は現在、チャーチ＝チューリングのテーゼとして知られている。

決定問題の起源は、17世紀に機械式計算機を成功裏に構築した後、数学的命題の真偽値を決定するために記号を操作できる機械を構築することを夢見たゴットフリート・ライプニッツに遡ります。 ^{[ 3 ]}彼は、最初のステップは明確な形式言語でなければならないことに気づき、その後の彼の研究の多くはその目標に向けられました。1928年、デイヴィッド・ヒルベルトとヴィルヘルム・アッカーマンは、上記の形式でこの問題を提起しました。

ヒルベルトは自身の「プログラム」を継続し、1928年の国際会議で3つの質問を提起した。そのうち3番目の質問は「ヒルベルトの決定問題」として知られるようになった。^{[ 4 ]} 1929年、モーゼス・シェーンフィンケルは、ポール・ベルネイスが準備した決定問題の特殊なケースに関する論文を発表した。^{[ 5 ]}

1930年になっても、ヒルベルトは解決不可能な問題など存在しないと信じていた。^{[ 6 ]}

この問いに答えるためには、「アルゴリズム」という概念を正式に定義する必要があった。これは、 1935年にアロンゾ・チャーチが自身のλ計算に基づく「有効計算可能性」の概念で、そして翌年にはアラン・チューリングがチューリングマシンの概念で行った。チューリングは、これらが計算の等価モデルであることをすぐに認識した。

決定問題に対する否定的な答えは、1935～36年にアロンゾ・チャーチによって与えられ（チャーチの定理）、その後まもなく1936年にアラン・チューリングによって独立に与えられました（チューリングの証明）。チャーチは、与えられた2つのλ計算式が等価であるかどうかを判定する計算可能な関数は存在しないことを証明しました。彼は、スティーブン・クリーネの以前の研究に大きく依拠しました。チューリングは、決定問題を解くことができる「アルゴリズム」または「一般的な方法」の存在という問題を、与えられたチューリングマシンが停止するかどうかを判定する「一般的な方法」の存在という問題（停止問題）に還元しました。 「アルゴリズム」がチューリングマシンとして表現できる方法を意味すると理解され、後者の質問に対する答えが（一般に）否定的であるならば、決定問題に対するアルゴリズムの存在に関する質問も（一般に）否定的でなければならない。チューリングは1936年の論文で次のように述べている。「各計算機『it』に対応して、我々は式『Un(it)』を構築し、もし『Un(it)』が証明可能かどうかを判定する一般的な方法が存在するならば、『it』が0を出力することがあるかどうかを判定する一般的な方法が存在することを示す」。

チャーチとチューリングの研究は、クルト・ゲーデルの不完全性定理に関する初期の研究、特に論理を算術に還元するために論理式に数値を割り当てる方法（ゲーデル番号付け）に大きく影響を受けていた。

決定問題は、ディオファントス方程式に解が存在するかどうかを判定するアルゴリズムを求めるヒルベルトの第10問題に関連しています。ユーリ・マティヤセヴィッチ、ジュリア・ロビンソン、マーティン・デイヴィス、ヒラリー・パトナムらの研究によって、そのようなアルゴリズムは存在しないことが確立され、1970年に証明の最終部分が完成しました。このことは、決定問題に対する否定的な答えも意味します。

演繹定理を用いると、決定問題は、与えられた一階述語論理の文が、与えられた有限個の文の論理的帰結であるかどうかを判定するという、より一般的な問題を包含するが、無限個の公理を持つ一階述語論理の妥当性は、直接決定問題に還元することはできない。このようなより一般的な決定問題は、実際的な関心事である。アルゴリズムで判定可能な一階述語論理もいくつかあり、その例としては、プレスバーガー算術、実閉体、多くのプログラミング言語の静的型システムなどが挙げられる。一方、ペアノの公理によって表現される加算と乗算を持つ自然数の一階述語論理は、アルゴリズムで判定することはできない。

デフォルトでは、このセクションの引用は Pratt-Hartmann (2023) からのものです。^{[ 7 ]}

古典的な決定問題は、与えられた一階論理式がすべてのモデルで真であるかどうかを問うものです。有限問題は、それがすべての有限モデルで真であるかどうかを問うものです。トラクテンブロートの定理は、これも決定不可能であることを示しています。^{[ 8 ] [ 7 ]}

いくつかの表記法：${\displaystyle {\rm {{Sat}(\Phi )}}}$これは、一連の論理式に対してモデルが存在するかどうかを判断する問題を意味する。${\displaystyle \Phi }$。${\displaystyle {\rm {{FinSat}(\Phi )}}}$これは同じ問題だが、有限モデルの場合である。${\displaystyle {\rm {Sat}}}$論理断片の問題は、各論理断片について判定できるプログラムが存在する場合に判定可能と呼ばれます。${\displaystyle \Phi }$断片内の有限個の論理式、${\displaystyle {\rm {{Sat}(\Phi )}}}$か否か。

決定可能性には階層構造が存在する。最上位には決定不可能な問題があり、その下には決定可能な問題がある。さらに、決定可能な問題は複雑性の階層に分類することができる。

論理式のクラスに対する実用的な判定手順を持つことは、プログラム検証や回路検証において非常に重要です。純粋なブール論理式は、通常、DPLLアルゴリズムに基づくSATソルバー技術を用いて判定されます。

より一般的な一階理論の決定問題については、線形実数または有理数演算上の連言式はシンプレックス法を用いて決定でき、線形整数演算（プレスバーガー演算）の式はクーパーのアルゴリズムまたはウィリアム・ピューのオメガテストを用いて決定できます。否定、連言、選言を含む式は充足可能性テストの難しさと連言の決定の難しさを併せ持っています。これらは現在では一般的にSMTソルビング技術を用いて決定されます。SMTソルビング技術はSATソルビングと連言の決定手順および伝播技術を組み合わせたものです。実多項式演算（実閉体理論とも呼ばれる）は決定可能です。これはタルスキー・ザイデンベルクの定理であり、円筒代数分解を用いてコンピュータに実装されています。

• 自動定理証明
• ヒルベルトの第二の問題
• オラクルマシン
• チューリングの証明

• デヴィッド・ヒルベルト;アッカーマン、ヴィルヘルム(1928)。Grundzüge der theoretischen Logik [数理論理学の原理] (ドイツ語)。スプリンガー・フェルラーグ。ISBN 0821820249。{{cite book}}ISBN /日付の不一致（ヘルプ）
• アッカーマン、ヴィルヘルム（1954）。決定問題の解決可能なケース。アムステルダム：ノースホランド。
• アロンゾ・チャーチ、「初等整数論における解決不可能な問題」、アメリカ数学ジャーナル、58（1936）、345-363ページ
• アロンゾ・チャーチ、「決定問題に関する覚書」、記号論理学ジャーナル、1（1936）、40-41頁。
• デイビス、マーティン（2001）。論理のエンジン：数学者とコンピュータの起源。ノートンペーパーバック（ノートンペーパーバック 版として初版刊行）。ニューヨーク、ニューヨーク、ロンドン：ノートン。ISBN 978-0-393-32229-3。
• アラン・チューリング、「計算可能な数について、決定問題への応用」、ロンドン数学会紀要、第2シリーズ、42（1936～37年）、230～265ページ。オンライン版：ジャーナルウェブサイト、チューリングデジタルアーカイブ、abelard.orgより。正誤表は第2シリーズ、43（1937年）、544～546ページに掲載。
• マーティン・デイビス著、『決定不能性：決定不能命題、解決不能問題、計算可能関数に関する基礎論文集』、レイヴン・プレス、ニューヨーク、1965年。チューリングの論文はこの巻の3番目に掲載されている。ゲーデル、チャーチ、ロッサー、クリーネ、ポストらの論文も収録されている。
• ホッジス、アンドリュー（1983）。アラン・チューリング：謎。ニューヨーク：サイモン＆シュスター。ISBN 978-0-671-49207-6。アラン・M・チューリングの伝記。彼の証明に至るまでの経緯と議論については、「真理の精神」の章を参照のこと。
• Soare, Robert I.、「計算可能性と再帰」、Bull. Symbolic Logic 2 (1996)、no. 3、284–321。
• トゥールミン、スティーブン、「天才の没落」、アンドリュー・ホッジス著「アラン・チューリング：エニグマ」の書評、ニューヨーク・レビュー・オブ・ブックス、1984年1月19日、 3ページ以降。
• ホワイトヘッド、アルフレッド・ノース、ラッセル、バートランド、『プリンキピア・マテマティカ』第56巻、ケンブリッジ大学出版局、1962年。パラドックスの問題に関して、著者らは、集合がその「決定関数」のいずれにおいても対象にならないという問題について議論している。特に、「序論、第1章、24ページ「形式論理で生じる困難」」、第2章I「悪循環原理」、37ページ以降、および第2章VIII「矛盾」、 60ページ 以降。 

• Wiktionaryにおけるentscheidungspblemの辞書定義