在數學和計算機科學中，可判定性（發音為 [?nt??a??d??sp?o?ble?m]，德語為“決策問題”）是 David Hilbert 和 Wilhelm Ackermann 在 1928 年提出的一個挑戰。該問題要求一種算法，考慮作為輸入， 陳述和回答是或否根據陳述是否普遍有效，即在滿足公理的每個結構中都有效。

根據一階邏輯完備性定理，一個命題普遍有效當且僅當它可以從公理中推導出來，所以可判斷性也可以看作是要求一個算法來決定給定命題是否可證明 使用邏輯規則的公理。

1936 年，Alonzo Church 和 Alan Turing 發表了獨立的論文，表明不可能通過圖靈機可計算的函數（或等價地，可表示為 lambda 演算）。 這個假設現在被稱為丘奇-圖靈論題。

可判定性的起源可以追溯到 17 世紀的戈特弗里德·萊布尼茨 (Gottfried Leibniz)，他在建造了一臺成功的機械計算器之后，夢想建造一臺可以操縱符號以確定數學陳述的真值的機器。 他意識到xxx步必須是一種干凈的形式化語言，他隨后的大部分工作都朝著這個目標邁進。 1928 年，大衛希爾伯特和威廉阿克曼以上述形式提出了這個問題。

在他的計劃的延續中，希爾伯特在 1928 年的一次國際會議上提出了三個問題，其中第三個問題被稱為希爾伯特的判定性。 1929 年，Moses Sch?nfinkel 發表了一篇關于決策問題特例的論文，該論文由 Paul Bernays 撰寫。

直到 1930 年，希爾伯特還相信不存在無法解決的問題。

在回答這個問題之前，必須正式定義算法的概念。 這是由 Alonzo Church 在 1935 年基于他的 λ 演算提出的有效可計算性概念完成的，第二年由 Alan Turing 提出了他的圖靈機概念。 圖靈立即意識到這些是等效的計算模型。

1935-36 年，Alonzo Church 給出了“不確定性”的否定答案（Church 定理），此后不久，Alan Turing 于 1936 年獨立給出了答案（圖靈證明）。 Church 證明了對于兩個給定的 λ-演算表達式，不存在決定它們是否等價的可計算函數。 他嚴重依賴 Stephen Kleene 的早期工作。 圖靈將能夠解決不確定性的“算法”或“通用方法”的存在問題簡化為確定任何給定圖靈機是否停止的“通用方法”的存在問題 或不（停止問題）。 如果“算法”被理解為表示可以表示為圖靈機的方法，并且對后一個問題的回答是否定的（通常），那么關于可判定性的算法是否存在的問題也必須 是負面的（一般來說）。 圖靈在他 1936 年的論文中說：對應于每個計算機器 'it'，我們構造了一個公式 'Un(it)' 并且我們表明，如果有一種通用方法可以確定 'Un(it) ' 是可證明的，那么有一種通用方法可以確定 'it' 是否曾打印過 0。

Church 和 Turing 的工作都深受 Kurt G?del 早期關于他的不完備性定理的工作的影響，特別是通過將數字（G?del 編號）分配給邏輯公式以將邏輯簡化為算術的方法。

不確定性與希爾伯特的第十個問題有關，該問題要求一種算法來確定丟番圖方程是否有解。 由 Yuri Matiyasevich、Julia Robinson、Martin Davis 和 Hilary Putnam 的工作建立的這種算法的不存在，以及 1970 年的最終證明，也暗示了對可判定性的否定回答。

一些一階理論是算法可判定的； 這方面的例子包括 Presburger 算術、實封閉域和許多編程語言的靜態類型系統。 然而，用皮亞諾公理表達的自然數的一般一階理論不能用算法來決定。

對邏輯公式的類別進行實用的決策程序對于程序驗證和電路驗證具有相當大的意義。 純布爾邏輯公式通常使用基于 DPLL 算法的 SAT 求解技術來確定。 線性實數或有理算術上的合取公式可以使用單純形算法確定，線性整數算術（Presburger 算術）中的公式可以使用 Cooper 算法或 William Pugh 的 Omega 檢驗確定。