În matematică și informatică, problema deciziei, denumită și (, din germană) este o provocare lansată de David Hilbert în 1928.Hilbert and Ackermann Problema cere un algoritm care are ca intrare o afirmație într-o logică de ordinul întâi (eventual cu un număr finit de axiome în afara axiomelor obișnuite din logica de ordinul întâi) și răspunde cu "Da" sau "Nu" după cum afirmația este universal valabilă, adică valabile în orice structură care satisface axiomele. Conform , o afirmație este universal valabilă dacă și numai dacă ea poate fi dedusă din axiome, deci problema deciziei poate fi văzută și ca cerând unui algoritm să decidă dacă o anumită afirmație este demonstrată din axiome cu ajutorul regulilor logicii.
În 1936, Alonzo Church și Alan Turing au publicat independent lucrăriChurch's paper was presented to the American Mathematical Society on 19 April 1935 and published on 15 April 1936. Turing, who had made substantial progress in writing up his own results, was disappointed to learn of Church's proof upon its publication (see correspondence between and Church in Alonzo Church papers ). Turing quickly completed his paper and rushed it to publication; it was received by the Proceedings of the London Mathematical Society on 28 May 1936, read on 12 November 1936, and published in series 2, volume 42 (1936–7); it appeared in two sections: in Part 3 (pages 230–240), issued on Nov 30, 1936 and in Part 4 (pages 241–265), issued on Dec 23, 1936; Turing added corrections in volume 43 (1937), pp. 544–546. See the footnote at the end of Soare: 1996. în care arătau că o soluție generală a problemei deciziei este imposibilă, presupunând că noțiunea intuitivă de „” este capturată de funcțiile calculabile de către o mașină Turing (sau, echivalent, de cele exprimate în ). Această ipoteză este acum cunoscut sub numele de teza Church–Turing.
Istoria problemei Originea problemei deciziei datează de la Gottfried Leibniz, care, în secolul al XVII-lea, după ce a construit o mecanică, visa să construiască o mașină care ar putea manipula simboluri pentru a determina valoarea de adevăr a unei afirmații matematice.Davis 2000: pp. 3–20 El și-a dat seama că primul pas ar trebui să fie un limbaj formal curat, și o mare parte din lucrările sale ulterioare s-au îndreptat în direcția acestui obiectiv. În 1928, David Hilbert și Wilhelm Ackermann au pus problema în forma prezentată mai sus.
În continuarea „programului” său, Hilbert a pus trei întrebări la o conferință internațională în 1928, dintre care a treia a devenit cunoscută sub numele de „ a lui Hilbert”.Hodges p. 91 În 1929, a publicat un articol cu privire la cazurile particulare ale problemei deciziei, care au fost pregătite de Paul Bernays.
Chiar și în 1930, Hilbert credea că nu există probleme de nerezolvat.Hodges p. 92, quoting from Hilbert
Răspunsul negativ Înainte ca întrebarea să poate primi răspuns, trebuia definită formal noțiunea de „algoritm”. Acest lucru a fost făcut de către Alonzo Church în 1936 cu conceptul de „calculabilitate efectivă”, bazat pe , precum și de către Alan Turing în același an, cu conceptul său de mașină Turing. Turing a recunoscut imediat că acestea sunt echivalente.
Răspunsul negativ la problema deciziei apoi a fost dat de către Alonzo Church în 1935-36 și la scurt timp după aceea de către Alan Turing în 1936. Church a demonstrat că nu există nicio funcție calculabilă care decide, pentru două λ-expresii date, dacă acestea sunt echivalente sau nu. El s-a bazat în mare măsură pe lucrările anterioare ale lui Stephen Kleene. Turing a redus întrebarea la existența unui „algoritm” sau a unei „metode generale” capabilă să rezolve problema deciziei la întrebarea dacă există sau nu o metodă generală care decide dacă o anumită mașină Turing se oprește sau nu (problema opririi). Dacă cuvântul „algoritm” este înțeles ca fiind echivalent cu o mașină Turing, și în condițiile în care întrebarea din urmă are răspuns negativ (în general), întrebarea despre existența unui algoritm pentru problema opririi are răspuns tot negativ (în general). În articolul său din 1936, Turing spunea: „Corespunzător fiecărei mașini de calcul «it» vom construi o formulă «Un(it)» și vom arăta că, dacă există o metodă generală pentru a determina dacă «Un(it)» este demonstrabilă, atunci există o metodă generală pentru a determina dacă «it» tipărește vreodată 0".
Munca lui Church și Turing a fost puternic influențată de lucrările anterioare ale lui Kurt Gödel la , mai ales prin metoda de atribuire de numere (o ) formulelor logice, în scopul de a reduce logica la aritmetică.
Problema deciziei este legată de , care cere un algoritm pentru a decide dacă au o soluție. Inexistența unui astfel de algoritm, stabilită de către în 1970, implică, de asemenea, un răspuns negativ la problema deciziei.
Unele teorii de ordinul întâi sunt algoritmic decidabile; exemple în acest sens includ , și ale multor limbaje de programare. Teoria generală de ordinul întâi a numerelor naturale exprimată prin nu poate fi decisă însă cu un algoritm.
Proceduri practice de decizie Existența unor proceduri practice de decizie pentru unele clase formule logice este însă de interes considerabil pentru și a circuitelor. Formulele pur booleene sunt, de obicei, decise folosind tehnici de rezolvare SAT bazate pe . Formulele conjunctive peste aritmetici liniare reale sau raționale pot fi decis cu ajutorul algoritmului simplex, formulele în aritmetica liniară a întregilor () pot fi decise cu ajutorul algoritmului lui Cooper sau cu testul Omega al lui . Formulele cu negații, conjuncții și disjuncții combină dificultățile testării satisfiabilității cu cele ale deciziei conjuncțiilor; ele sunt, în general, decise astăzi folosind tehnici de , care combina rezolvările SAT cu procedurile de decizie pentru conjuncții și tehnici de propagare. Aritmetica polinomială reală cunoscută și ca „teoria ”, este decidabilă; aceasta este , care a fost pusă în aplicare în computere cu ajutorul .
Note
Bibliografie David Hilbert și Wilhelm Ackermann (1928). Grundzüge der theoretischen Logik (Principii de Logică Matematică). Springer-Verlag, . Alonzo Church, "O problemă de nerezolvat de elementar de teoria numerelor", American Journal of Mathematics, 58 (1936), pp 345-363 Alonzo Church, "O notă privind Entscheidungsproblem", Revista de Logica Simbolică, 1 (1936), pp. 40-41. Martin Davis, 2000, Motoare de Logica, W. W. Norton & Company, Londra, pbk. Alan Turing, "On computable numbers, cu o cerere la Entscheidungsproblem", Proceedings of the London Mathematical Society, Seria 2, 42 (1936-7), pp 230-265. Versiunile Online: de la site-ul revistei, de la Turing Arhivă Digitală, de la abelard.org . Erata a apărut în Seria 2, 43 (1937), pp 544-546. Martin Davis, "Nehotărât, Bază Documente privind Nehotărât Propuneri, Probleme de Nerezolvat Și Calculabil Funcții", Raven Press, New York, 1965. Turing hârtie este #3 în acest volum. Documentele includ pe cele de Gödel, Church, Rosser, Kleene, și Post. Andrew Hodges, Alan Turing: The Enigma, Simon and Schuster, New York, 1983. Alan M. Turing biografia lui. Cf Capitolul "Duhul Adevărului" pentru o istorie care să conducă la, și o discuție a lui dovada. Robert Soare, "Computability și recursivitate", Bull. Logica simbolică 2 (1996), nr. 3, 284-321. Stephen Toulmin, "Căderea unui Geniu", o recenzie de carte "Alan Turing: The Enigma de Andrew Hodges", în The New York Review of Books, 19 ianuarie 1984, p. 3ff. Alfred North Whitehead și Bertrand Russell, Principia Mathematica a *56, la Cambridge University Press, 1962. Re: problema de paradoxuri, autorii discuta problema dintr-un set nu fi un obiect în orice "determinarea funcții", în special "Introducere, Cap. 1 p. 24 "...dificultățile care apar în logica formală", și Chap. 2.I. "Vicios-Cerc Principiul" p. 37ff, și Chap. 2.VIII. "Contradicțiile" p. 60 ff.
Categorie:Gottfried Leibniz Categorie:Logică matematică