У матэматыцы і інфарматыцы, Праблема вырашальнасці (ням.: Entscheidungsproblem - нямецкая для “праблемы вырашэння”) — задача з вобласці падстаў матэматыкі, сфармуляваная Давідам Гільбертам і Вільгельмам Акерманам у 1928 годзе: знайсці алгарытм, які б прымаў у якасці ўваходных дадзеных апісанне любой фармальнай мовы і матэматычнага сцвярджэння «S» на гэтай мове - і, пасля канчатковага ліку крокаў, спыняўся б, і выдаваў адзін з двух адказаў: «Так» або «Не», - у залежнасці ад таго, цi з’яўляецца зацверджанне «S» заўсёды сапраўдным, гэта значыць сапраўдным у кожнай структуры, якая задавальняе аксіёмы. [1]. Адказ не патрабуе абгрунтаванняў, але павінен быць дакладным.
Такі алгарытм мог бы, на прыклад, пацвердзіць гіпотэзу Гольдбаха і гіпотэзу Рымана нягледзячы на тое, што доказы (і абвяржэння) пакуль невядомыя. Неразвязальнасць праблемы вырашальнасці (невырашальнасць мноства праўдзівых формул арыфметыкі) для мовы арыфметыкі, якая змяшчае «роўнасць», «складанне» і «множанне», з’яўляецца следствам неарыфметычнасцi гэтага мноства. Неарыфметычнасць з’яўляецца следствам тэарэмы Тарскага аб невыказальнасцi паняцця праўдзівасці ў мове сродкамі той жа мовы» [2].
Згодна з тэарэмай паўнаты логікі першага парадку, сцвярджэнне з’яўляецца агульнасапраўдным тады і толькі тады, калі яго можна вывесці з аксіём, таму праблему вырашальнасці таксама можна разглядаць як запыт пра алгарытм, якi вырашыць, ці даказана дадзенае сцвярджэнне з аксіём, выкарыстоўваючы правілы логікі.
У 1936 годзе — Алонза Чорч і незалежна ад яго Алан Цьюрынг апублікавалі працы [3], у якіх паказалі, што не існуе алгарытму для вызначэння праўдзівасці сцвярджэнняў арыфметыкі, а таму і больш агульная праблема вырашальнасці таксама не мае рашэння. Гэты вынік атрымаў назву: «тэарэма Чорча — Цьюрынга».
Паходжанне праблемы вырашальнасці ўзыходзіць да Готфрыда Лейбніца, які ў XVII стагоддзі пасля пабудовы паспяховай механічнай вылічальнай машыны марыў пабудаваць машыну, якая можа маніпуляваць сімваламі дзеля таго, каб вызначыць праўдзівасць матэматычных выказванняў. [4] Ён зразумеў, што першым крокам павінна быць вызначэнне чыстай фармальнай мовы, і большая частка яго наступнай працы была накіравана на гэтую мэту. У 1928 г. Дэвід Гільберт і Вільгельм Акерман паставілі пытанне ў форме, выкладзенай вышэй.
У працяг сваёй “праграмы” Гільберт паставіў тры пытанні на міжнароднай канферэнцыі ў 1928 г., трэцяе з якіх стала называцца “Гільбертавай праблемай вырашальнасці.” [5] У 1929 г. Майсей Шэйнфiнкель апублікаваў артыкул пра асаблівыя выпадкі праблемы вырашальнасці, падрыхтаваны Паулем Бернайсам. [6]
Ужо ў 1930 г. Гільберт лічыў, што не можа быць невырашальнай праблемы. [7]
Перш чым можна было адказаць на пытанне вырашальнасці, трэба было фармальна вызначыць паняцце “алгарытм”. Гэта зрабiў Алонза Чорч у 1935 г. з канцэпцыяй “эфектыўнай вылічальнасці”, заснаванай на яго λ-вылічэнні, і Алан Цьюрынг ў наступным годзе з яго канцэпцыяй машыны Цьюрынга с. Цьюрынг адразу зразумеў, што гэта эквівалентныя мадэлі вылічэнняў.
Адмоўны адказ на вырашэнне праблемы вырашальнасці быў дадзены Алонзам Чорчам ў 1935-36 ( ‘Тэарэма Чорча’ ) і незалежна неўзабаве пасля гэтага Аланам Цьюрынгам у 1936 г. ( доказ Цьюрынга ). Чорч даказаў, што не існуе вылічальнай функцыі, якая вырашае для двух дадзеных выразаў λ-вылічэння, эквівалентныя яны ці не. Ён у значнай ступені абапіраўся на ранейшыя працы Стывена Кліна. Цьюрынг звёў пытанне аб існаванні “агульнага метаду”, які вырашае, ці спыняецца якая-небудзь машына Цьюрынга (праблема спынення), да пытання пра існаванне “алгарытму” альбо “агульнага метаду”, здольнага вырашыць праблему вырашальнасці. Калі “Алгарытм” разумеецца як эквівалент машыны Цюрынга, а адказ на апошняе пытанне адмоўны (ўвогуле), тады i на пытанне аб існаванні алгарытму для праблемы вырашальнасці адказ таксама павінны быць адмоўным у цэлым. У сваёй працы 1936 г. Цьюрынг кажа: “Адпаведна кожнай вылічальнай машыне «it», мы ствараем формулу «Un(it)» і паказваем, што калі існуе агульны метад вызначэння даказальнасцi «Un(it)», тады існуе i агульны метад вызначэння таго, ці надрукуе «it» калі-небудзь 0 “.
На працу Чорча і Цьюрынга моцна паўплывала больш ранняя праца Курта Гёдэля над яго Тэарэмай незавершанасці, асабліва метадам прысваення лікаў нумерацыi Гёдэля да лагічных формул, каб звесці логіку да арыфметыкі.
Праблема вырашальнасці звязана з дзесятай праблемай Гільберта, якая запытвае алгарытм, ці мае ўраўненне Дыяфанта вырашэнне. Неіснаванне такога алгарытму, усталяванае Юрыям Матыясевічам у 1970 г., таксама прадугледжвае адмоўны адказ на праблему вырашальнасці.
Некаторыя тэорыі першага парадку можна алгарытмічна вырашаць; прыклады гэтага ўключаюць арыфметыку Прэсбургера, рэальнае закрытае поле s і сістэмы статычнага тыпу з многіх моваў праграмавання. Агульную тэорыю першага парадку натуральнага ліку, выражаную ў аксіёмах Пеано, нельга вырашыць з дапамогай алгарытму.
Цэннай уяўляецца наяўнасць практычных працэдур прыняцця рашэнняў для класаў лагічных формул для праверкі праграмы і праверкі схем. Чыстыя лагічныя формулы звычайна вырашаюцца з выкарыстаннем методык праблемы выкананасці булевых формул, заснаваных на поўным алгарытме пошуку з вяртаннем. Кан’юнктыўныя формулы над лінейнай рэальнай альбо рацыянальнай арыфметыкай можна вырашыць, выкарыстоўваючы сімплексны алгарытм, формулы ў лінейнай цэлалiкавай арыфметыцы (арыфметыка Прэсбургера) можна вырашыць, выкарыстоўваючы алгарытм Купера альбо тэст Амега Уільяма П’ю. Формулы з адмаўленнямі, злучнікамі і дыз’юнкцыямі спалучаюць цяжкасці праверкі выкананасці з праблемамі рашэння злучнікаў; яны звычайна вырашаюцца ў наш час з выкарыстаннем рашэння тэорыi модуля выкананасці , якія спалучаюць рашэнне тэорыi модуля выкананасці з працэдурамі прыняцця рашэнняў для спалучэння і метадаў распаўсюджвання. Сапраўдная паліномная арыфметыка, таксама вядомая як тэорыя рэальнага замкнёнага поля s, можа быць вырашана; гэта тэарэма Тарскага – Зайдэнберга, якая была рэалізавана ў кампутарах з выкарыстаннем цыліндрычнага алгебраічнага раскладання.