Mantıksal Akıl Yürütme ve Teorem İspatı
Mantıksal akıl yürütme ve teorem ispatı, bilgiyi temsil etmek için biçimsel mantığın kullanılmasını ve bir öncüller kümesinden zorunlu olarak çıkan sonuçların türetilmesi olan çıkarımın otomasyonunu ele almaktadır.
Tanım
Teorem ispatı, tipik olarak formüllerin sağlam çıkarım kurallarıyla manipüle edilmesi yoluyla, bir mantıksal formülün bir aksiyomlar kümesinden çıkıp çıkmadığının otomatik olarak türetilmesidir; bu işlem, hedefe ulaşılana veya bir çelişkiye varılana kadar devam etmektedir.
Kapsam
Bu konu, önermeler ve birinci dereceden mantıkta akıl yürütmeyi ve bunu otomatikleştiren algoritmaları kapsamaktadır: önermeler mantığı için doğruluk tablosu ve DPLL tabanlı tatmin edilebilirlik kontrolü, birinci dereceden mantık için birleştirme (unification) ve çözünürlük ilkesi (resolution principle), ileri ve geri zincirleme ile mantık programlamanın temelleri. Çıkarım prosedürlerinin sağlamlığı, tamlığı ve karar verilebilirliği ele alınmaktadır. Belirsizliği veya varsayılanları tolere eden akıl yürütme, belirsizlik altında akıl yürütme ve monotonik olmayan akıl yürütme ile ilgili konularda işlenmektedir.
Temel sorular
- Bir sonucun bir öncüller kümesi tarafından gerektirilmesi ne anlama gelmektedir ve gerektirme mekanik olarak nasıl kontrol edilmektedir?
- Çözünürlük ilkesi, birleştirme ile birlikte, birinci dereceden mantık için tek bir tam çıkarım kuralını nasıl sağlamaktadır?
- İleri ve geri zincirleme, çıkarım stratejileri olarak nasıl farklılaşmaktadır?
- Birinci dereceden geçerliliğin sadece yarı-karar verilebilir olduğu göz önüne alındığında, otomatik akıl yürütmenin sınırları nelerdir?
Anahtar kavramlar
- önermeler ve birinci dereceden mantık
- gerektirme ve geçerlilik
- birleştirme (unification)
- çözünürlük (resolution) ve çürütme (refutation)
- DPLL ve SAT çözme
- ileri ve geri zincirleme
- Horn cümleleri ve mantık programlama
- sağlamlık ve tamlık
Temel kuramlar
- Çözünürlük ilkesi
- Robinson'ın çözünürlüğü, birleştirme ile birleştiğinde birinci dereceden mantık için çürütme-tam olan cümleler üzerindeki tek bir çıkarım kuralıdır: herhangi bir tatmin edilemez cümleler kümesi, boş cümlenin türetilmesiyle tatmin edilemez olarak gösterilebilmektedir.
- DPLL ve önermeler mantığı tatmin edilebilirliği
- Davis-Putnam prosedürü ve onun DPLL iyileştirmesi, birim yayılımı (unit propagation) ve saf-literal eliminasyonu (pure-literal elimination) ile sistematik durum ayırma (case splitting) yoluyla önermeler mantığı tatmin edilebilirliğini belirlemekte ve modern SAT çözücülerin temelini oluşturmaktadır.
- Mantık programlama ve geri zincirleme
- Birinci dereceden mantığı Horn cümleleriyle sınırlamak ve hedefleri geriye doğru çözümlemek, hesaplamanın ispat arayışı olduğu mantık programlamayı ortaya çıkarmaktadır; bu da hem bir akıl yürütme yöntemi hem de bir programlama paradigması sağlamaktadır.
Klinik önem
Otomatik teorem ispatı ve SAT/SMT çözümü, donanım ve yazılım doğrulaması, program analizi, planlama ve matematikte kullanılmaktadır; Prolog gibi mantık programlama dilleri ise veri tabanlarına, ayrıştırmaya ve kural tabanlı sistemlere geri zincirleme çıkarımını uygulamaktadır.
Tarihçe
Gilmore, Davis ve Putnam (1960) tarafından geliştirilen erken ispat prosedürleri, önermeler ve niceleyici akıl yürütmeyi otomatikleştirdi ve Robinson'ın çözünürlük ilkesi (1965), birinci dereceden çıkarımı tek bir kuralda birleştirdi. 1970'lerde çözünürlük, mantık programlama ve Prolog'a dönüştürüldü; SAT ve SMT çözümü daha sonra önemli bir pratik teknoloji haline geldi.
Öne çıkan isimler
- John Alan Robinson
- Martin Davis
- Hilary Putnam
- Robert Kowalski
- Alan Robinson
İlgili konular
Temel eserler
- robinson1965
- davis1960
- kowalski1979
Sıkça sorulan sorular
- Çözünürlük ilkesi nedir?
- Çözünürlük, tamamlayıcı literaller içeren iki cümleyi alıp geri kalanları birleştiren yeni bir cümle üreten tek bir çıkarım kuralıdır. Birleştirme ile tekrar tekrar uygulandığında, bir birinci dereceden cümleler kümesinin tatmin edilemez olduğunu gösterebilmektedir; bu da çürütme yoluyla teorem ispatlamanın temelini oluşturmaktadır.
- Otomatik teorem ispatının sonlanması garanti edilmekte midir?
- Önermeler mantığı için geçerlilik karar verilebilir olduğundan, prosedürler sonlanmaktadır. Tam birinci dereceden mantık için geçerlilik sadece yarı-karar verilebilirdir: tam bir ispatlayıcı sonunda herhangi bir geçerli formülü doğrulayacaktır, ancak geçersiz bir formül üzerinde sonsuza kadar çalışabilir, bu nedenle genel olarak sonlanma garanti edilmemektedir.