İçeriğe atla

Otomatikleştirilmiş muhakeme

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 akıl yürütmenin en gelişmiş alt alanları, otomatik teorem ispatlama ve otomatik ispatın denetlenmesidir.Benzetme indüksiyonu ile mantık yürütmede kapsamlı çalışmalar yapılmıştır.

Otomatik akıl yürütme araçları ve teknikleri olarak klasik mantıksal hesaplamalar, bulanık mantık, Bayes çıkarımı, maksimal entropi gibi konular listelenebilir.

Uygulamaları

Otomatik akıl yürütme, otomatik teorem kanıtlayıcıları oluşturmak için sıklıkla kullanılmıştır. Bununla birlikte, çoğu zaman, teorem kanıtlarının etkili olabilmesi için bazı insan rehberliğine ihtiyaç duyar ve bu yüzden daha genel olarak kanıt yardımcıları olarak nitelendirilir. Bazı durumlarda, bu kanıtlayıcılar bir teoremin kanıtlanması için yeni yaklaşımlar geliştirebilirler.Mantık Kuramcısı(Logic Theorist) bunun güzel bir örneğidir.Bu program sayesinde, Principia Mathematica'daki Whitehead ve Russell tarafından sağlanan kanıttan daha etkili olan ve daha az adım gerektiren kanıt üretmek mümkün olmuştur.Mantık, matematik ve bilgisayar bilimleri, mantık programlama, yazılım ve donanım doğrulama, devre tasarımı ve daha birçok konuda giderek artan sayıda problemi çözmek için otomatik akıl yürütme programları uygulanmaktadır.

İ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">Bilgisayar bilimi</span> belirli evren kurallarına dayalı, sistematik çalışan ve elementlerin ya da ağların birbirleriyle olan ilişkisi

Bilgisayar bilimi, bilgisayarların tasarımı ve kullanımı için temel oluşturan teori, deney ve mühendislik çalışmasıdır. Hesaplamaya ve uygulamalarına bilimsel ve pratik bir yaklaşımdır. Bilgisayar bilimi; edinim, temsil, işleme, depolama, iletişim ve erişimin altında yatan yönteme dayalı prosedürlerin veya algoritmaların fizibilitesi, yapısı, ifadesi ve mekanizasyonunun sistematik çalışmasıdır. Bilgisayar biliminin alternatif, daha özlü tanımı "büyük, orta veya küçük ölçekli algoritmik işlemleri otomatikleştirme çalışması" olarak nitelendirilebilir. Bir bilgisayar bilimcisi, hesaplama teorisi ve hesaplama sistemlerinin tasarımı konusunda uzmanlaşmıştır.

Bilişim, bilişim bilimi ya da bilgisayar bilimi, bilgi ve hesaplamanın kuramsal temellerini ve bunların bilgisayar sistemlerinde uygulanabilmeleri sağlayan pratik teknikleri araştıran bir yapısal bilim dalıdır. Bilişimciler ya da bilgisayar bilimcileri bilgi oluşturan, tanımlayan ve dönüştüren algoritmik süreçler icat edip, kompleks sistemleri tasarlamak ve modellemek için uygun soyutlamalar formüle ederler. Bilişim Dünya'da hızla gelişmeye devam eden önemli bir teknolojidir.

Sinyaller ve sistemler kavram ve teorisi diğer birçok mühendislik ve bilim dallarıyla birlikte, elektrik ve elektronik mühendisliğinin hemen her alanında ve Biyomedikal mühendisliğinin tıbbi cihazlar ve biyoelektrik gibi elektrikle ilgilenen alt disiplinlerinde gerekli olup, haberleşme, EKG, EEG gibi tıbbi cihazlar, devreler ve sistemler ve kontrol sistemleri gibi alanlardaki ileri düzeyde çalışmaların matematiksel temelini oluşturur.

<span class="mw-page-title-main">Yapay zekâ</span> insani zekaya sahip makine ve yazılım geliştiren bilgisayar bilimleri dalı

Yapay zekâ ya da kısaca YZ,, insanlar da dahil olmak üzere hayvanlar tarafından, doğal zekânın aksine makineler tarafından görüntülenen zekâ çeşididir. İlk ve ikinci kategoriler arasındaki ayrım genellikle seçilen kısaltmayla ortaya çıkar. Güçlü yapay zeka genellikle Yapay genel zekâ olarak etiketlenirken, doğal zekayı taklit etme girişimleri yapay biyolojik zekâ olarak adlandırılır. Önde gelen yapay zeka ders kitapları, alanı zeki etmenlerin çalışması olarak tanımlar: Çevresini algılayan ve hedeflerine başarıyla ulaşma şansını en üst düzeye çıkaran eylemleri gerçekleştiren herhangi bir cihaz. Halk arasında, yapay zekâ kavramı genellikle insanların insan zihni ile ilişkilendirdiği öğrenme ve problem çözme gibi bilişsel eylemleri taklit eden makineleri tanımlamak için kullanılır.

<span class="mw-page-title-main">Bilgi</span> İnsan aklının erebileceği olgu, gerçek ve ilkelerin bütünü

Bilgi, genellikle geçerliliği veya doğruluğu varsayılacak şekilde mümkün olan en yüksek kesinlik derecesi ile karakterize edilen, kişiler veya gruplar için mevcut olan bir dizi gerçek. Bilginin tanımı kullanıldığı alana ve bakış açılarına göre değişiklik göstermektedir. Epistemolojide subje ile obje arasındaki ilişkiden doğan her türlü ürüne denir. Bilginin doğası, kökenleri ve boyutları ile ilgilenen dala epistemoloji adı verilir.

<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">Alan Turing</span> İngiliz matematikçi, bilgisayar bilimcisi ve kriptolog

Alan Mathison Turing, İngiliz matematikçi, bilgisayar bilimcisi ve kriptolog. Bilgisayar biliminin kurucusu sayılır. Geliştirmiş olduğu Turing testi ile makinelerin ve bilgisayarların düşünme yetisine sahip olup olamayacakları konusunda bir kriter öne sürmüştür.

<i>Petitio principii</i> Döngüsel Mantık Safsatası

Petitio principii, kalıplaşmış Latince bir terimdir. Döngüsel nedensellikten doğan safsatayı tanımlar. Bir sonuca neden olan şeyi, o sonucu ispatlamakta kullanma safsatasıdır. Safsatalarla doğru bilgi edinilemez ve bir yere varılamaz. Safsataya giren döngüsel akıl yürütmeler kendi kendilerini ürettikleri için, bir nevi kuyruğunu yakalamaya çalışan aptal bir tilki gibi olduklarından sağlıklı akıl yürütmeler değildirler.

Eleştirel düşünme akıl yürütme, analiz ve değerlendirme gibi zihinsel süreçlerden oluşan bir düşünme biçimidir. Eleştirel düşünme yerine kimi zaman tartışma mantığı ya da biçim dışı (enformel) mantık terimleri de kullanılmaktadır. Sorgulama ve şüpheciliğe dayanan eleştirel düşünme sağduyu ve bilimsel kanıtlarla uyuşan net hükümlere varmak için somut veya soyut konular üzerinde düşünme süreçlerini de içermektedir. Bu yönüyle diğer bir düşünme biçimi olan yaratıcı düşünmeyi tamamlamaktadır.

Bilişsel psikoloji, düşünme, hissetme, öğrenme, anımsama, karar verme, dil, problem çözme ve yargılama gibi zihinsel süreçlerin en geniş anlamda incelenmesidir. Yani bilişsel psikologlar insanların bilgiyi anlama, saklama ve bilincine geri getirmeleriyle ilgilenirler. Bilişsel psikologlar zihinsel süreçlerin incelenebileceğine ve incelenmesi gerektiğine inanırlar. Her ne kadar bilişsel süreçler doğrudan gözlenemeseler de, davranışlar gözlenebilir ve bu davranışların altında yatan bilişsel süreçler hakkında çıkarımlar yapılabilir.

<span class="mw-page-title-main">Dağıtık hesaplama</span>

Dağıtık hesaplama bilişim biliminde dağıtık sistemleri inceleyen bir bilim dalıdır. Dağıtık sistem, birden fazla otomatik bilgisayarın bir ağ üzerindeki iletişimidir. Ağdaki bilgisayarlar belirli bir hedefe ulaşmak için birbirleriyle etkileşim içerisindedirler. Dağıtık sistemi çalıştıran bilgisayar programına dağıtık program denir. Bu tür programları yazma işlemine dağıtık programlama adı verilir.

<span class="mw-page-title-main">Hesaplamalı dilbilim</span>

Bilgisayarlı dilbilim veya hesaplamalı dilbilim, doğal dilin istatistiksel veya kural tabanlı modelleme yöntemleriyle ve hesaplamalı bir perspektif ile inceleyen disiplinler arası bir bilgisayar bilimi alanıdır.

Windows kabuğu, Microsoft Windows işletim sisteminin grafik kullanıcı arabirimidir. Kolay tanımlanabilir öğeleri, masaüstü, görev çubuğu, Başlangıç menüsü, görev değiştirici ve Otomatik yürütme özelliğini içerir. Windows'un bazı sürümlerinde ayrıca Flip 3D ve takılar da bulunuyor. Bununla birlikte, Windows kabuğu, Windows'ta çalışan bilgisayar programlarının kabuk nesnelerinin hiyerarşisi yoluyla bilgisayarın kaynaklarına erişmesini sağlayan bir kabuk ad alanını da uygular. "Masaüstü" hiyerarşinin en üst nesnesidir; bunun altında, diskte saklanan bir dizi dosya ve klasörlerin yanı sıra içeriği sanal veya dinamik olarak oluşturulmuş bir dizi özel klasör bulunur. Geri Dönüşüm Kutusu, Kütüphaneler, Denetim Masası, Bilgisayarım ve Ağ gibi kabuk nesnelerine örnektir.

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.

Bu, Wikipedia'da yer alan sayı teorisi konularıyla ilgili sayfaların bir listesidir.

Otomatik akıl yürütme, bilgisayar biliminin 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.

<span class="mw-page-title-main">Bilgi temsili ve akıl yürütme</span> Dünya ile ilgili bilgileri karmaşık görevleri çözmek için kullanabilecekleri bir biçimde temsil etmeye adanmış yapay zeka

Bilgi temsili ve akıl yürütme, dünyayla ilgili bilgilerin bir bilgisayar sistemi tarafından anlaşılıp işlenebilecek şekilde ifade edilmesini hedefleyen yapay zeka alanıdır. Bilgi temsili bir bilgisayar destekli sağlık teşhisi ya da doğal dilde konuşma gibi karmaşık yapay zeka problemlerinin çözülmesinde kilit rol oynar. Bilgi temsili araştırmaları, insanların problemleri nasıl çözdüğünü anlamak için psikolojiden yardım alır ve karmaşık sistemleri basitleştirecek matematiksel biçimler geliştirir. Aynı zamanda mantık bulgularını kullanarak çeşitli akıl yürütme biçimlerini otomatikleştirir.

<span class="mw-page-title-main">Sarit Kraus</span>

Sarit Kraus, İsrail'deki Bar-İlan Üniversitesinde bilgisayar bilimi profesörüdür. Bu alanlarda örnek hizmet ve liderliğinin yanı sıra yapay zekâya, özellikle çok aracılı sistemlere, insan-aracı etkileşimine, otonom aracılara ve monoton olmayan akıl yürütmeye yaptığı katkılardan dolayı 2020-2021 ACM Athena Öğretim Görevlisi seçilmiştir.

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.