Robinson'un çözüm prosedürünün eksiklikleri nelerdi?
Paulson ve diğerleri. LCF'den Isabelle / HOL'e şunu söyleyin:
Birinci dereceden mantık için çözüm, ilke olarak tam, ancak pratikte sıklıkla hayal kırıklığı yaratıyor.
Bence tam, herhangi bir gerçek formülü birinci dereceden mantıkta doğru kanıtlayabilecekleri anlamına gelir. In Otomatik Akıl Handbook I bulmak:
Çözünürlük, çürütme açısından eksiksiz bir teoremi kanıtlama yöntemidir: bir çelişki (yani boş cümle), herhangi bir tatmin edilemez cümle kümesinden çıkarılabilir.
Wikipedia'dan:
Tatmin edilebilir bir birinci dereceden formülün tatmin edilemez olduğunu kanıtlamaya çalışmak, sonlandırıcı olmayan bir hesaplama ile sonuçlanabilir.
Bu neden hayal kırıklığı yaratıyor?
Yanıtlar
"Uygulamada hayal kırıklığı" kesinlikle resmi olarak tanımlanamazken, "tam" ın aksine (bu aslında "her gerçek formülü kanıtlayabilir" anlamına gelir), naif çözümlemenin uzaktan bile yeterli olmadığı örnekleri, yani olması gereken örnekleri bulmak oldukça kolaydır. kanıtlaması kolay, ancak hangi çözünürlüğün aşırı derecede yavaş olduğu.
Ünlü bir örnek bir kodlama güvercin deliği prensibine için$n$ önerme mantığındaki boşluklar (bu ifade "$n+1$ güvercinler sığamaz $n$kopyasız delikler). Bu ifadenin yalnızca alt üstel zaman içinde çözünürlüğü kullanan bir kanıtı yoktur$n$.
Herhangi bir hızlı çözünürlük kanıtı olmadan ifadeleri bulmanın çok kolay olduğu yüklem mantığında işler daha da kötüdür.
Herhangi bir çözümleme uygulamasının çözücüleri seçmek için bir strateji uygulaması gerektiğine dikkat edin, ki bu zaten çok zor bir problemdir ve aktif bir araştırma alanıdır, çünkü teoremi kanıtlamak için en pratik algoritmalar , hiper çözünürlük gibi saf çözünürlük geliştirmeleridir .