Entscheidungsproblem - Entscheidungsproblem - Wikipedia

İçinde matematik ve bilgisayar Bilimi, Entscheidungsproblem (telaffuz edildi [ɛntˈʃaɪ̯dʊŋspʁoˌbleːm], Almanca "karar problemi" için) David Hilbert ve Wilhelm Ackermann 1928'de.^[1] Sorun bir algoritma girdi olarak bir ifadeyi dikkate alan ve ifadenin olup olmadığına göre "Evet" veya "Hayır" yanıtını veren evrensel olarak geçerliyani her yerde geçerlidir yapı aksiyomları tatmin etmek.

Tamlık teoremi

Tarafından birinci dereceden mantığın tamlık teoremi, bir ifade, ancak ve ancak aksiyomlardan çıkarılabilirse evrensel olarak geçerlidir. Entscheidungsproblem Ayrıca, belirli bir ifadenin aksiyomlardan kanıtlanabilir olup olmadığına karar vermek için bir algoritma istemek olarak da görülebilir. mantık kuralları.

1936'da, Alonzo Kilisesi ve Alan Turing yayınlanan bağımsız makaleler^[2] genel bir çözüm olduğunu göstermek Entscheidungsproblem "sezgisel" kavramının "etkili bir şekilde hesaplanabilir "bir tarafından hesaplanabilen işlevler tarafından yakalanır Turing makinesi (veya eşdeğer olarak, içinde ifade edilebilenler tarafından lambda hesabı ). Bu varsayım artık Kilise-Turing tezi.

Sorunun tarihi

Kökeni Entscheidungsproblem geri döner Gottfried Leibniz başarılı bir mekanik inşa ettikten sonra on yedinci yüzyılda hesaplama makinesi, semboller üzerinde işlem yapabilen bir makine yapmayı hayal etti. gerçek değerler matematiksel ifadeler.^[3] İlk adımın temiz olması gerektiğini fark etti. resmi dil ve sonraki çalışmalarının çoğu bu amaca yönelikti. 1928'de, David Hilbert ve Wilhelm Ackermann soruyu yukarıda özetlenen biçimde sordu.

Hilbert, "programının" devamında, 1928'de uluslararası bir konferansta üç soru sordu ve üçüncüsü "Hilbert's Entscheidungsproblem."^[4] 1929'da, Moses Schönfinkel Karar sorununun özel durumlarına ilişkin bir makale yayınladı. Paul Bernays.^[5]

1930 gibi geç bir tarihte Hilbert, çözülemez sorun diye bir şeyin olmayacağına inanıyordu.^[6]

Olumsuz cevap

Soru cevaplanmadan önce, "algoritma" kavramının resmi olarak tanımlanması gerekiyordu. Bu tarafından yapıldı Alonzo Kilisesi 1935'te "etkin hesaplanabilirlik" kavramı ile λ-hesap ve gelecek yıl Alan Turing tarafından konseptiyle Turing makineleri. Turing bunların eşdeğer olduğunu hemen anladı hesaplama modelleri.

Olumsuz cevap Entscheidungsproblem 1935–36'da Alonzo Kilisesi tarafından verildi (Kilise teoremi) ve bağımsız kısa bir süre sonra Alan Turing tarafından 1936'da (Turing'in kanıtı ). Kilise olmadığını kanıtladı hesaplanabilir işlev verilen iki λ-kalkülüs ifadesi için eşdeğer olup olmadıklarına karar verir. Daha önceki çalışmalarına büyük ölçüde güvendi. Stephen Kleene. Turing, herhangi bir Turing Makinesinin durup durmayacağına karar veren 'genel bir yöntemin' varlığı sorununu azaltmıştır ( durdurma sorunu ) sorunu çözebilecek bir 'algoritma' veya 'genel yöntem' varlığı sorusuna Entscheidungsproblem. 'Algoritma' bir Turing Makinesine eşdeğer olarak anlaşılırsa ve ikinci sorunun cevabıyla (genel olarak), bir Algoritmanın varlığı hakkındaki soru Entscheidungsproblem ayrıca negatif olmalıdır (genel olarak). Turing 1936 tarihli makalesinde şöyle diyor: "Her bir bilgi işlem makinesine karşılık gelen 'it' bir 'Un (it)' formülü oluşturuyoruz ve 'Un (it)' in kanıtlanabilir olup olmadığını belirlemek için genel bir yöntem varsa, o zaman belirlemek için genel bir yöntem olduğunu gösteriyoruz. "o" hiç 0 yazdırır mı ".

Hem Kilise'nin hem de Turing'in çalışmaları, Kurt Gödel daha önceki çalışmaları eksiklik teoremi özellikle sayı atama yöntemiyle (bir Gödel numaralandırma ) mantığı aritmetiğe indirgemek için mantıksal formüllere.

Entscheidungsproblem ile ilgilidir Hilbert'in onuncu problemi, soran algoritma karar vermek Diofant denklemleri bir çözüm var. Böyle bir algoritmanın yokluğu, Yuri Matiyasevich 1970 yılında, Entscheidungsproblem'e olumsuz bir yanıt anlamına da gelir.

Bazı birinci dereceden teoriler algoritmik olarak karar verilebilir; bunun örnekleri şunları içerir Presburger aritmetiği, gerçek kapalı alanlar ve statik tip sistemler çoğunun Programlama dilleri. Genel birinci dereceden teorisi doğal sayılar olarak ifade edildi Peano'nun aksiyomları ancak bir algoritma ile karar verilemez.

Pratik karar prosedürleri

Mantıksal formül sınıfları için pratik karar prosedürlerine sahip olmak, program doğrulama ve devre doğrulama. Saf Boole mantıksal formüllerine genellikle SAT çözme dayalı teknikler DPLL algoritması. Doğrusal gerçek veya rasyonel aritmetik üzerinden birleşik formüllere şu şekilde karar verilebilir: simpleks algoritması, doğrusal tamsayı aritmetiğindeki formüller (Presburger aritmetiği ) kullanılarak karar verilebilir Cooper'ın algoritması veya William Pugh 's Omega testi. Olumsuzluklar, bağlaçlar ve ayrılıklar içeren formüller, tatmin edilebilirlik testinin zorluklarını bağlaçların kararının zorluklarıyla birleştirir; genellikle günümüzde SMT çözme SAT-çözmeyi, bağlaçlar ve yayılma teknikleri için karar prosedürleriyle birleştiren teknikler. Gerçek polinom aritmetik, aynı zamanda teorisi olarak da bilinir. gerçek kapalı alanlar, karar verilebilir; bu Tarski-Seidenberg teoremi, bilgisayarlarda uygulanmış olan silindirik cebirsel ayrıştırma.

Ayrıca bakınız

• Karar verilebilirlik (mantık)
• Otomatik teorem kanıtlama
• Hilbert'in ikinci sorunu
• Oracle makinesi
• Turing'in kanıtı

Notlar

Referanslar

• David Hilbert ve Wilhelm Ackermann (1928). Grundzüge der theoretischen Logik (Matematiksel Mantığın İlkeleri). Springer-Verlag, ISBN  0-8218-2024-9.
• Alonzo Kilisesi, "Çözülemeyen bir sorun temel sayı teorisi ", American Journal of Mathematics, 58 (1936), s. 345–363
• Alonzo Kilisesi, "Entscheidungsproblem üzerine bir not", Journal of Symbolic Logic, 1 (1936), s. 40–41.
• Martin Davis, 2000, Mantık Motorları, W.W. Norton & Company, Londra, ISBN  0-393-32229-7 pbk.
• Alan Turing, "Hesaplanabilir Sayılar Üzerine, Entscheidungsproblem Uygulaması ile ", Tutanaklar Londra Matematik Derneği, Seri 2, 42 (1936–7), s. 230–265. Çevrimiçi sürümler: dergi web sitesinden, Turing Digital Archive'dan, abelard.org'dan. Errata Seri 2, 43 (1937), s. 544–546'da yayınlandı.
• Martin Davis, "Karar Verilemeyen Öneriler, Çözülemeyen Sorunlar ve Hesaplanabilir Fonksiyonlar Üzerine Kararsız, Temel Makaleler", Raven Press, New York, 1965. Turing'in makalesi bu ciltte 3 numaradır. Makaleler arasında Gödel, Church, Rosser, Kleene ve Post'un yazıları bulunmaktadır.
• Andrew Hodges, Alan Turing: Enigma, Simon ve Schuster, New York, 1983. Alan M. Turing'in biyografisi. Kanıtına götüren bir tarih ve bunun bir tartışması için "Gerçeğin Ruhu" bölümüne bakın.
• Robert Soare, "Hesaplanabilirlik ve özyineleme", Bull. Symbolic Logic 2 (1996), no. 3, 284–321.
• Stephen Toulmin, "Fall of a Genius", bir kitap incelemesi "Alan Turing: Enigma Andrew Hodges ", The New York Review of Books, 19 Ocak 1984, s. 3ff.
• Alfred North Whitehead ve Bertrand Russell, Principia Mathematica to * 56, Cambridge, University Press, 1962. Re: paradoks problemi, yazarlar bir setin problemini "belirleme fonksiyonlarının" hiçbirinde bir nesne olmadığını tartışıyor, özellikle "Giriş, Böl. 1 s. 24 "... biçimsel mantıkta ortaya çıkan zorluklar" ve Bölüm 2.I. "Kısır Döngü İlkesi" s. 37ff ve Bölüm 2.VIII. "Çelişkiler" s. 60 ff.

Dış bağlantılar

• Sözlük tanımı entscheidungsproblem Vikisözlük'te