Otomatik muhakeme - Automated reasoning
Gelen bilgisayar bilimleri , özellikle bilgi gösterimi ve akıl yürütme ve metalogic , alanı otomatik muhakeme farklı yönlerini anlamak adamıştır akıl . Otomatik akıl yürütme çalışması, bilgisayarların tamamen veya neredeyse tamamen otomatik olarak akıl yürütmesine izin veren bilgisayar programlarının üretilmesine yardımcı olur . Otomatik akıl yürütme, yapay zekanın bir alt alanı olarak görülse de, teorik bilgisayar bilimi ve felsefesi ile de bağlantıları vardır .
Otomatik akıl yürütmenin en gelişmiş alt alanları, otomatik teorem kanıtlama (ve etkileşimli teorem kanıtlamanın daha az otomatik ancak daha pragmatik alt alanı ) ve otomatik kanıt denetimidir (sabit varsayımlar altında garantili doğru akıl yürütme olarak görülür). Tümevarım ve kaçırma kullanarak benzetme yoluyla akıl yürütme konusunda da kapsamlı çalışmalar yapılmıştır .
Diğer önemli konular, belirsizlik altında akıl yürütme ve monoton olmayan akıl yürütmeyi içerir. Belirsizlik alanının önemli bir kısmı, daha standart otomatik kesintinin üzerine daha fazla minimallik ve tutarlılık kısıtlamalarının uygulandığı argümantasyon alanıdır. John Pollock'un OSCAR sistemi, yalnızca otomatik bir teorem ispatlayıcısı olmaktan daha spesifik olan otomatik bir argümantasyon sisteminin bir örneğidir.
Otomatik akıl yürütme araçları ve teknikleri, klasik mantık ve hesap, bulanık mantık , Bayes çıkarımı , maksimum entropi ile akıl yürütme ve daha az resmi ad hoc tekniklerini içerir.
İlk yıllar
Gelişimi formel mantık kendisinin gelişmesine yol açmıştır otomatik muhakeme, alanında büyük bir rol oynamıştır yapay zeka . Bir resmi kanıtı her mantıksal çıkarım temel geri kontrol edildiği bir kanıtıdır aksiyomlar matematik. İstisnasız tüm ara mantıksal adımlar sağlanır. Sezgiden mantığa çeviri rutin olsa bile sezgiye başvurulmaz. Bu nedenle, resmi bir kanıt daha az sezgiseldir ve mantıksal hatalara daha az duyarlıdır.
Bazıları, birçok mantıkçıyı ve bilgisayar bilimcisini bir araya getiren 1957 Cornell Yaz toplantısını otomatik akıl yürütmenin veya otomatik tümdengelimin kaynağı olarak görüyor . Diğerleri, bundan önce , Newell, Shaw ve Simon'ın 1955 Mantık Teorisi programıyla veya Martin Davis'in 1954'te Presburger'in karar prosedürünü uygulamasıyla (ki bu, iki çift sayının toplamının çift olduğunu kanıtladı) başladığını söylüyor.
Otomatik muhakeme, önemli ve popüler bir araştırma alanı olmasına rağmen , seksenlerde ve doksanların başlarında bir " AI kışı " geçirdi. Ancak alan daha sonra yeniden canlandı. Örneğin, 2005 yılında Microsoft , iç projelerinin çoğunda doğrulama teknolojisini kullanmaya başladı ve 2012 Visual C sürümüne mantıksal bir belirtim ve kontrol dili eklemeyi planlıyor.
Önemli katkılar
Principia Mathematica , Alfred North Whitehead ve Bertrand Russell tarafından yazılan biçimsel mantıkta bir dönüm noktası çalışmasıydı. Principia Mathematica - ayrıca anlam Matematik İlkeleri - tümünü veya bir kısmını elde etmek bir amaç ile yazılmıştır matematiksel ifadeler açısından, sembolik mantık . Principia Mathematica ilk olarak 1910, 1912 ve 1913'te üç cilt halinde yayınlandı.
Mantık Kuramcısı (LT), 1956'da Allen Newell , Cliff Shaw ve Herbert A. Simon tarafından teoremleri ispatlamada "insan akıl yürütmesini taklit etmek" içingeliştirilen ilk programdıve Principia Mathematica'nın ikinci bölümünden elli iki teorem üzerinde gösterildi ve otuz kanıtladı. - sekiz tanesi. Program, teoremleri kanıtlamaya ek olarak, Whitehead ve Russell tarafından sağlanandan daha zarif olan teoremlerden biri için bir kanıt buldu. Sonuçlarını yayınlamak için başarısız bir girişimden sonra, Newell, Shaw ve Herbert 1958'deki The Next Advance in Operation Research adlı yayınlarındaşunlarıbildirdiler:
- "Artık dünyada düşünen, öğrenen ve yaratan makineler var. Üstelik, bu şeyleri yapma yetenekleri (görünür bir gelecekte) üstesinden gelebilecekleri problemlerin kapsamı genişleyene kadar hızla artacaktır. insan zihninin uygulandığı aralık."
Resmi Kanıt Örnekleri
Yıl teorem Prova Sistemi resmileştirici Geleneksel Kanıt 1986 İlk Eksiklik Boyer-Moore Shankar Gödel 1990 ikinci dereceden karşılıklılık Boyer-Moore Russinoff Eisenstein 1996 Calculus'un Temelleri HOL Işık Harrison tavuk stoğu 2000 Cebirin Temelleri Mizar Milewski Brynski 2000 Cebirin Temelleri Coq Geuvers et al. Kneser 2004 Dört Renk Coq Gonthier Robertson ve ark. 2004 Asal sayı Isabelle Avigad et al. Selberg - Erdös 2005 Ürdün Eğrisi HOL Işık Hales Thomassen 2005 Brouwer Sabit Nokta HOL Işık Harrison Kuhn 2006 sinek lekesi 1 Isabelle Bauer - Nipkow Hales 2007 Cauchy Kalıntısı HOL Işık Harrison Klasik 2008 Asal sayı HOL Işık Harrison analitik kanıt 2012 Feit Thompson Coq Gonthier et al. Bender, Glauberman ve Peterfalvi 2016 Boolean Pisagor üçlüleri sorunu SAT olarak resmileştirildi Heule et al. Hiçbiri
Prova sistemleri
- Boyer-Moore Teoremi Kanıtı (NQTHM)
- NQTHM'nin tasarımı John McCarthy ve Woody Bledsoe'dan etkilenmiştir. 1971'de Edinburgh, İskoçya'da başlatılan bu, Pure Lisp kullanılarak oluşturulmuş tam otomatik bir teorem ispatıydı . NQTHM'nin ana yönleri şunlardı:
- Lisp'in çalışma mantığı olarak kullanılması.
- toplam özyinelemeli fonksiyonlar için bir tanım ilkesine güven.
- yeniden yazma ve "sembolik değerlendirme"nin kapsamlı kullanımı.
- sembolik değerlendirmenin başarısızlığına dayanan bir tümevarım buluşsal yöntemi.
- HOL Işık
- Yazılı OCaml , HOL Işık bir sade ve net mantıksal temeli ve düzenli bir uygulama olması tasarlanmıştır. Esasen klasik yüksek mertebeden mantık için başka bir ispat yardımcısıdır.
- Coq
- Fransa'da geliştirilen Coq , çalıştırılabilir programları spesifikasyonlardan Objective CAML veya Haskell kaynak kodu olarak otomatik olarak çıkarabilen başka bir otomatik doğrulama yardımcısıdır . Özellikler, programlar ve kanıtlar, Endüktif Yapıların Hesabı (CIC) adı verilen aynı dilde resmileştirilir.
Uygulamalar
Otomatik muhakeme, otomatikleştirilmiş teorem ispatlayıcıları oluşturmak için en yaygın şekilde kullanılmıştır. Bununla birlikte, çoğu zaman, teorem kanıtlayıcılar, etkili olmak için bazı insan rehberliğine ihtiyaç duyar ve bu nedenle daha genel olarak kanıt yardımcıları olarak nitelendirilir . Bazı durumlarda, bu tür ispatlayıcılar bir teoremi ispatlamak için yeni yaklaşımlar geliştirmiştir. Mantık Teorisi buna iyi bir örnektir. Program, Principia Mathematica'daki teoremlerden biri için Whitehead ve Russell tarafından sağlanan kanıttan daha verimli (daha az adım gerektiren) bir kanıt buldu. Resmi mantık, matematik ve bilgisayar bilimi, mantık programlama , yazılım ve donanım doğrulama, devre tasarımı ve diğer birçok alanda artan sayıda sorunu çözmek için otomatik akıl yürütme programları uygulanmaktadır . TPTP (Sutcliffe ve Suttner 1998) düzenli olarak güncellenen bu tür sorunların bir kütüphanedir. CADE konferansında düzenli olarak düzenlenen otomatik teorem kanıtlayıcılar arasında da bir rekabet vardır (Pelletier, Sutcliffe ve Suttner 2002); yarışma için problemler TPTP kütüphanesinden seçilir.
Ayrıca bakınız
- Otomatik makine öğrenimi (AutoML)
- Otomatik teorem ispatı
- muhakeme sistemi
- anlamsal akıl yürütücü
- Program analizi (bilgisayar bilimi)
- Yapay zeka uygulamaları
- Yapay zekanın ana hatları
- Casuistry • Vaka temelli muhakeme
- Abdüktif akıl yürütme
- çıkarım motoru
- sağduyulu akıl yürütme
Konferanslar ve çalıştaylar
- Otomatik Akıl Yürütme Uluslararası Ortak Konferansı (IJCAR)
- Otomatik Kesinti Konferansı (CADE)
- Uluslararası Analitik Tablolar ve İlgili Yöntemlerle Otomatik Akıl Yürütme Konferansı
dergiler
Topluluklar
Referanslar
- ^ Defourneaux, Gilles ve Nicolas Peltier. " Otomatik kesintide analoji ve kaçırma ." IJCAI (1). 1997.
- ^ John L. Pollock
- ^ C. Hales, Thomas "Biçimsel Kanıt" , Pittsburgh Üniversitesi. 2010-10-19 tarihinde alındı
- ^ a b "Otomatik Kesinti (AD)" , [PRL Projesinin Doğası] . 2010-10-19 tarihinde alındı
- ^ Martin Davis (1983). "Otomatik Kesintilerin Tarih Öncesi ve Erken Tarihi". Jörg Siekmann'da; G. Wrightson (ed.). Akıl Yürütme Otomasyonu (1) — Hesaplamalı Mantık 1957–1966 Üzerine Klasik Makaleler . Heidelberg: Springer. s. 1-28. ISBN'si 978-3-642-81954-4. burada: s.15
- ^ "Principia Mathematica" , Stanford Üniversitesi'nde . 2010-10-19 alındı
- ^ "Mantık Kuramcısı ve Çocukları" . 2010-10-18 alındı
- ^ Shankar, Natarajan Küçük Kanıt Motorları , Bilgisayar Bilimleri Laboratuvarı, SRI International . 2010-10-19 alındı
- ^ Shankar, N. (1994), Metamathematics, Machines, and Gödel's Proof , Cambridge, UK: Cambridge University Press, ISBN 9780521585330
- ^ Russinoff, David M. (1992), "Kuadratik Karşılıklılığın Mekanik Kanıtı", J. Autom. Sebep. , 8 (1): 3-21, doi : 10.1007/BF00263446
- ^ Gonthier, G.; ve diğerleri (2013), "Odd Order Theorem'in Makine Kontrollü Kanıtı" (PDF) , Blazy, S.; Paulin-Mohring, C.; Pichardie, D. (eds.), Interactive Theorem Proving , Lecture Notes in Computer Science, 7998 , pp. 163–179, doi : 10.1007/978-3-642-39634-2_14 , ISBN 978-3-642-39633-5
- ^ Heule, Marijn JH ; Kullmann, Oliver; Marek, Victor W. (2016). "Boolean Pisagor Üçlü Problemini Küp ve Fethet Yoluyla Çözme ve Doğrulama". Tatmin Edilebilirlik Testinin Teorisi ve Uygulamaları – SAT 2016 . Bilgisayar Bilimleri Ders Notları. 9710 . s. 228–245. arXiv : 1605.00723 . doi : 10.1007/978-3-319-40970-2_15 . ISBN'si 978-3-319-40969-6.
- ^ Boyer-Moore Teoremi Kanıtı . 2010-10-23 tarihinde alındı
- ^ Harrison, John HOL Light: genel bir bakış . 2010-10-23 alındı
- ^ Coq'a Giriş . 2010-10-23 alındı
- ^ Otomatik Akıl Yürütme , Stanford Ansiklopedisi . 2010-10-10 alındı