İçeriğe atla

Otomatik akıl yürütme

Otomatik akıl yürütme, bilgisayar biliminin (bilgi temsilini ve akıl yürütmeyi içerir) ve akıl yürütmenin farklı yönlerini anlamaya çalışan bir alandır. 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 çeşitli yöntemler kullanılarak benzetme yoluyla akıl yürütme konusunda da kapsamlı çalışmalar yapılmıştır.[1]

Diğer önemli konular arasında belirsizlik altında akıl yürütme ve monoton olmayan akıl yürütme yer alır. 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ığı tartışma alanıdır. John Pollock'un OSCAR sistemi,[2] yalnızca otomatik bir teorem ispatlayıcısı olmaktan daha spesifik olan otomatik bir tartışma sisteminin bir örneğidir.

Otomatik akıl yürütme araçları ve teknikleri arasında klasik mantık ve hesap, bulanık mantık, Bayes çıkarımı, maksimum entropi ile akıl yürütme ve daha daha az resmi ad hoc teknikleri bulunur.

İlk yıllar

Biçimsel mantığın gelişimi, yapay zekanın gelişmesine yol açan otomatik akıl yürütme alanında büyük bir rol oynadı. Biçimsel bir kanıt, her mantıksal çıkarımın matematiğin temel aksiyomlarına geri döndürüldüğü bir kanıttır. İ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.[3]

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.[4] 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.[5]

Otomatik akıl yürütme, önemli ve popüler bir araştırma alanı olmasına rağmen, seksenlerde ve doksanların başlarında bir "Yapay zeka 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.[6]

Ö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ıdır. Principia Mathematica - aynı zamanda Matematik İlkeleri anlamına gelir - matematiksel ifadelerin tamamını veya bir kısmını sembolik mantık açısından türetmek amacıyla yazılmıştır. Principia Mathematica ilk olarak 1910, 1912 ve 1913'te üç cilt halinde yayınlanmıştır.[7]

Mantık Teorisi, 1956'da Allen Newell, Cliff Shaw ve Herbert A. Simon tarafından teoremleri ispatlamada "insan akıl yürütmesini taklit etmek" için geliştirilen ilk programdı ve Principia Mathematica'nın ikinci bölümünden elli iki teorem üzerinde gösterilmiştir. Bunlardan otuz sekiz tanesi kanıtlandı.[8] Program, teoremleri kanıtlamaya ek olarak, Whitehead ve Russell tarafından sağlanandan daha zarif olan teoremlerden biri için bir kanıt bulmuştur. 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. Ayrıca, (görünür bir gelecekte) baş edebilecekleri problemler yelpazesi insan zihninin uygulanmış olduğu menzil ile aynı seviyeye gelene kadar, bu şeyleri yapma yetenekleri hızla artacaktır."[9]

Biçimsel (Formal) kanıtlar
Yıl Teorem İspat sistemi Formalize eden Geleneksel Kanıt
1986 İlk Eksiklik Boyer-Moore Shankar[10]Gödel
1990 İkinci Dereceden Karşılıklılık Boyer-Moore Russinoff[11]Eisenstein
1996 Calculus'un Temelleri HOL Light Harrison Henstock
2000 Cebirin Temelleri Mizar Milewski Brynski
2000 Cebirin Temelleri Coq Geuvers et al. Kneser
2004 Dört Renk Coq Gonthier Robertson et al.
2004 Asal Sayı Isabelle Avigad et al. Selberg-Erdős
2005 Jordan Eğrisi HOL Light Hales Thomassen
2005 Brouwer Sabit Nokta HOL Light Harrison Kuhn
2006 Flyspeck 1 Isabelle Bauer- Nipkow Hales
2007 Cauchy Kalıntısı HOL Light Harrison Classical
2008 Asal Sayı HOL Light Harrison Analytic proof
2012 Feit-Thompson Coq Gonthier et al.[12]Bender, Glauberman and Peterfalvi
2016 Boolean Pisagor Üçlüleri Sorunu SAT Heule et al.[13]None

Kanıt sistemleri

Boyer-Moore Teoremi Kanıtı

NQTHM (Boyer-Moore Theorem Prover; 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ıdır. NQTHM'nin ana yönleri şunlardı:

  1. Lisp'in çalışma mantığı olarak kullanılması.
  2. Toplam özyinelemeli -fonksiyonlar için bir tanım ilkesine dayanma.
  3. Yeniden yazma ve "sembolik değerlendirme"nin kapsamlı kullanımı.
  4. Sembolik değerlendirmenin başarısızlığına dayanan bir tümevarım buluşsal yöntemi.[14]

HOL Light

OCaml'de yazılan HOL Light, basit ve temiz bir mantıksal temele ve düzenli bir uygulamaya sahip olacak şekilde tasarlanmıştır. Klasik yüksek mertebeden mantık için başka bir ispat yardımcısıdır.[15]

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 prova asistanıdır. Özellikler, programlar ve kanıtlar, Endüktif Yapıların Hesabı (Calculus of Inductive Constructions; CIC) adı verilen aynı dilde resmîleştirilir.[16]

Uygulamalar

Otomatik muhakeme, otomatikleştirilmiş teorem kanıtlayı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ğini gerektirmektedir. Bu nedenle daha genel olarak kanıt yardımcıları olarak nitelendirilmektedir. 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 bulmuştur. Biçimsel (Formel) mantık, matematik ve bilgisayar bilimleri, 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, düzenli olarak güncellenen bu tür problemlerin bir kütüphanesidir. 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çilmektedir.[17]

Kaynakça

  1. ^ Defourneaux, Gilles, and Nicolas Peltier. "Analogy and abduction in automated deduction." IJCAI (1). 1997.
  2. ^ "John L. Pollock". 12 Temmuz 2011 tarihinde kaynağından arşivlendi. 
  3. ^ Hales, Thomas C. "External Tools for the Formal Proof of the Kepler Conjecture". EasyChair. doi:10.29007/2l48. 
  4. ^ Baader, Franz, (Ed.) (2003). "Automated Deduction – CADE-19". Lecture Notes in Computer Science. doi:10.1007/b11829. ISSN 0302-9743. 
  5. ^ Rothlauf, Franz (2012). Automation of reasoning : classical papers on computational logic 19571966. [Place of publication not identified]: Springer. ISBN 3-642-81954-0. OCLC 802334981. 
  6. ^ "Automated Deduction (AD)", [The Nature of PRL Project]. Retrieved on 2010-10-19
  7. ^ "Principia Mathematica", at Stanford University. Retrieved 2010-10-19
  8. ^ ""The Logic Theorist and its Children"". 25 Mayıs 2003 tarihinde kaynağından arşivlendi. Erişim tarihi: 19 Haziran 2021. 
  9. ^ Shankar, Natarajan Little Engines of Proof, Computer Science Laboratory, SRI International. Retrieved 2010-10-19
  10. ^ Shankar, N. (1997). Metamathematics, machines, and Gödel's proof. 1st pbk. ed. Cambridge: Cambridge University Press. ISBN 0-521-58533-3. OCLC 37209144. 
  11. ^ Russinoff, DavidM. (1992-02). "A mechanical proof of Quadratic Reciprocity". Journal of Automated Reasoning (İngilizce). 8 (1). doi:10.1007/BF00263446. ISSN 0168-7433.
  12. ^ Interactive theorem proving : 4th International Conference, ITP 2013, Rennes, France, July 22-26, 2013. Proceedings. Sandrine Blazy, Christine Paulin-Mohring, David Pichardie. Berlin. 2013. ISBN 978-3-642-39634-2. OCLC 856650301. 
  13. ^ Theory and applications of satisfiability testing -- SAT 2016 : 19th International Conference, Bordeaux, France, July 5-8, 2016, Proceedings. Nadia Creignou, Daniel Le Berre. Switzerland. 2016. ISBN 978-3-319-40970-2. OCLC 951904034. 
  14. ^ "The Boyer- Moore Theorem Prover". 2 Eylül 2004 tarihinde kaynağından arşivlendi. 
  15. ^ "Harrison, John HOL Light: an overview" (PDF). 29 Eylül 2012 tarihinde kaynağından (PDF) arşivlendi. 
  16. ^ "Introduction to Coq". 20 Kasım 2009 tarihinde kaynağından arşivlendi. Erişim tarihi: 19 Haziran 2021. 
  17. ^ "Automated Reasoning". 18 Ağustos 2000 tarihinde kaynağından arşivlendi. Erişim tarihi: 19 Haziran 2021. 

İlgili Araştırma Makaleleri

<span class="mw-page-title-main">Matematik</span> nicelik, yapı, uzay ve değişim gibi konularla ilgilenen bilim dalı

Matematik ; sayılar, felsefe, uzay ve fizik gibi konularla ilgilenir. Matematikçiler ve filozoflar arasında matematiğin kesin kapsamı ve tanımı konusunda görüş ayrılığı vardır.

<span class="mw-page-title-main">Matematiksel ispat</span> ilgilenilen bir önermenin, belirli aksiyomlar esas alınarak, doğru olduğunu gösterme yöntemi

Matematiksel ispat, matematiksel bir ifade için türetilmiş varsayımların mantıksal olarak doğru olduğu sonucunu garantileyen, çıkarımsal bir argümandır. Argüman, teoremler gibi önceden oluşturulmuş diğer ifadeleri kullanabilir; lakin prensipte her delil, kabul edilen çıkarım kurallarıyla birlikte yalnızca aksiyom olarak bilinen belirli temel veya orijinal varsayımlar kullanılarak oluşturulabilir.

<span class="mw-page-title-main">Kurt Gödel</span> Avusturyalı-Amerikalı matematikçi (1906 – 1978)

Kurt Gödel, Avusturyalı-Amerikalı mantıkçı, matematikçi ve matematik felsefecisidir. Kendi ismiyle anılan Gödel'in Eksiklik Teoremi ile tanınır. Aristoteles'ten bu yana en büyük mantıkçılardan biri olarak kabul edilir.

Matematiksel mantık, biçimsel mantığın matematiğe uygulanmasıyla ilgilenen bir matematik dalıdır. Metamatematik, matematiğin temelleri ve kuramsal bilgisayar bilimi alanlarıyla yakınlık gösterir. Matematiksel mantığın temel konuları biçimsel sistemlerin ifade gücünün ve biçimsel ispat sistemlerinin tümdengelim gücünün belirlenmesidir.

<span class="mw-page-title-main">Mantık</span> bilginin yapısını inceleyen, doğru ile yanlış arasındaki akıl yürütmenin ayrımını yapan disiplin

Mantık ya da eseme, bilginin yapısını inceleyen, doğru ile yanlış arasındaki akıl yürütmenin ayrımını yapan disiplindir, doğru düşüncenin aletidir. Önceleri bir felsefe dalıyken daha sonra kendi başına bir ihtisas alanı olmuştur. Matematik ve bilgisayar biliminin de parçası haline gelmiştir. Bir disiplin olarak Aristoteles tarafından kurulmuştur. Aristoteles'den etkilenen Farabi tarafından iki kısımda kategorize edilmiştir. İbn-i Sina geçicilik ve içerme arasındaki ilişkiyi geliştirmiştir. Çağdaş zamanlarda Frege, Russell ve Wittgenstein önemli katkılar yapmıştır.

<span class="mw-page-title-main">Pierre de Fermat</span> Fransız matematikçi ve avukat

Pierre de Fermat, neredeyse eşitlik (“adequality”) tekniği de dahil olmak üzere sonsuz küçük hesaplara yol açan erken gelişmeler için yaptığı katkılarla bilinen bir Fransız matematikçiydi. Özellikle, eğri çizgilerin en büyük ve en küçük koordinatlarını bulmanın özgün bir yöntemini keşfetmesiyle tanınır; bu, o zamanlar bilinmeyen diferansiyel kalkülüsünkine benzer ve sayı teorisi üzerine yaptığı araştırmadır. Analitik geometri, olasılık ve optiğe kayda değer katkılarda bulundu. En çok ışık yayılımı hakkındaki Fermat ilkesi ve Diophantus'un Aritmeticasının bir kopyasının kenarındaki bir notta açıkladığı sayı teorisindeki Fermat'nın Son Teoremi ile tanınır. Aynı zamanda Fransa'nın Toulouse Parlamentosu'nda avukattı.

<span class="mw-page-title-main">Gottlob Frege</span>

Friedrich Ludwig Gottlob Frege, modern matematiksel mantığın ve analitik felsefenin kurucusu sayılan Alman matematikçi, mantıkçı ve filozof.

Programlama paradigmaları, programlama dillerini özelliklerine göre sınıflandırmanın bir yoludur. Diller birden fazla paradigma içinde sınıflandırılabilir.

<span class="mw-page-title-main">Argüman</span> ikna etmeye çalışmak ya da sabitleştirmek veya gerçek bir sonuca varmak

Mantık ve felsefede argüman; sonuç ve onun doğruluk derecesini belirlemeye yönelik verilen öncüllerden kurulmuş bir dizi ifadedir. Bir argüman ifadelerden oluşur. Bunlardan biri sonuç, diğerleri sonucun doğruluğuna dayanak olarak verilen öncüllerdir. Herhangi bir düşünceyle karşılaştığımızda, o düşüncenin içerdiği esas iddiayı ileten ifade argümanın sonucu; onu destekleyen diğer tüm ifadeler argümanın öncülleridir. Bir argümanın doğal dildeki mantıksal formu, sembolik biçimsel dilde temsil edilebilir ve doğal dilden bağımsız şekilde, matematik ve bilgisayar bilimlerinde biçimsel olarak tanımlanmış argümanlar yapılabilir.

Matematikte bir sabit nokta teoremi, bir F fonksiyonunun, genel terimlerle ifade edilmiş belli koşullar altında en az bir sabit noktası olduğunu ifade eden bir sonuçtur. Bu tür sonuçlar matematikte en çok kullanılanlar arasındadır.

Otomatikleştirilmiş muhakeme, otomatik akıl yürütmenin farklı yönlerinin izah edilmesine odaklanmış bir bilgisayar bilimi ve matematiksel mantık alanıdır. Otomatik akıl yürütme çalışması, bilgisayarların neredeyse tamamen otomatik olarak bilgisayar programları üretmesine yardımcı olur. Otomatik akıl yürütme, yapay zekanın bir alt alanı olarak düşünülmesine rağmen, teorik bilgisayar bilimi ve hatta felsefe ile de bağlantıları vardır.

Otomatik teorem kanıtlama, teoremlerin bilgisayar programları aracılığıyla kanıtlanmasına odaklanan matematiksel mantık dalıdır. Otomatik yordamlar için matematiksel kanıt yönteminin kullanılması bilgisayar biliminin gelişiminde kilit rol oynamıştır.

<span class="mw-page-title-main">Kelebek teoremi</span> Bir çemberin başka iki kirişinin üzerinden çizilen kirişin orta noktası hakkındaki teorem

Kelebek teoremi, Öklid geometrisinin klasik bir sonucudur ve aşağıdaki gibi ifade edilebilir:

Geometride demet teoremi; en basit durumda, gerçek Öklid düzlemindeki altı çember ve sekiz nokta üzerine bir ifadedir. Genel olarak, sadece oval Möbius düzlemleri tarafından meydana getirilen bir Möbius düzleminin bir özelliğidir. Demet teoremi Miquel teoremi ile karıştırılmamalıdır.

<span class="mw-page-title-main">Thoralf Skolem</span>

Thoralf Albert Skolem matematiksel mantık ve küme teorisi alanlarında çalışan Norveçli matematikçi.

Ernest Nagel Amerikalı bir bilim filozofuydu. Rudolf Carnap, Hans Reichenbach ve Carl Hempel ile birlikte, bazen mantıksal pozitivist hareketin en önemli figürlerinden biri olarak görülmektedir. 1961 tarihli Bilimin Yapısı adlı kitabı, bilimsel açıklama mantığında temel bir çalışma olarak kabul edilir.

Fiziksel bir sembol sistemi, fiziksel kalıpları kullanır, bu yapılarda birleştirir ve yeni ifadeler üretmek için onları manipüle etmektedir.

Bilgisayar biliminde, bildirimsel programlama bir programlama paradigmasıdır. —bilgisayar programlarının yapısını ve öğelerini oluşturma stili— bir hesaplamanın mantığını kontrol akışını tanımlamadan ifade eder.

Akıl yürütme psikolojisi, insanların nasıl akıl yürüttüğünün incelenmesidir ve genellikle geniş anlamda insanların sorunları nasıl çözdüğünü ve karar verdiğini bildirmek için sonuçlara varma süreci olarak tanımlanır. Psikoloji, felsefe, dilbilim, bilişsel bilim, yapay zeka, mantık ve olasılık teorisi ile örtüşmektedir.

Matematikte, Alman matematikçi David Hilbert tarafından 1920'lerin başında formüle edilen Hilbert'in programı, matematiğin temellerini açıklığa kavuşturmaya yönelik ilk girişimlerin tutarsız olduğu bulunduğunda, matematiğin temel krizine önerilen bir çözümdü. Çözüm olarak Hilbert, mevcut tüm teorileri sonlu, sonlu bir aksiyom dizisine dayandırmayı ve bu aksiyomların tutarlı olduğuna dair bir kanıt sunmayı önerdi. Hilbert, gerçek analiz gibi daha karmaşık sistemlerin tutarlılığının daha basit sistemleri kullanarak kanıtlayabileceğini gösterdi.Sonuçta matematiğin tamamının tutarlılığı temel aritmetiğe indirgenebilir.


Bu sayfa, bu Vikipedi makalesine dayanmaktadır.
Metin, CC BY-SA 4.0 lisansı altında mevcuttur; ek koşullar uygulanabilir.
Görseller, videolar ve sesler kendi lisansları altında mevcuttur.