Bölüm XII Niceleme Mantığı
Çözümleyici Çizelge
Çözümleyici çizelge yöntemimi Niceleme Mantığı'nda da kullanabiliriz. Eklem sembolleri ve onların değillemeleri üzerinden tanımlanmış 9 çözümleme kuralı yine geçerli olacaktır. Sadece, sembolik dilin yeni öğeleri olan Tümel Niceleyici, Tikel Niceleyici ve onların değillemeleri için ayrıca 4 çözümleme kuralı tanımlanacaktır.
Bir niceleyinin kendisinin ya da değilinin etki alanında olmayan önermelere eklem çözümleme kuralları uygulanır.
Örnek12.1
F(ab), G(ac) ∧ H(ab), F(ab) →( ¬G(ac) ∨ ¬H(ab)) önermelerinin çözümleyici çizelgesi
[Niceleyici Çözümleme (Özelleme) Kuralları]{.underline}
Tikel Özelleme (∃Ö)
∃xP(x)
P(a) (satır numarası, ∃Ö)
Tikel özellemede daha önce yol üzerinde bulunmayan bir ad sembolü kullanılmalıdır.
Tümel Özelleme (∀Ö)
∀xP(x)
P(a) (sıra numarası, ∀Ö)
Tümel özellemede herhangi bir ad sembolü kullanılabilir.
Aynı tümel önerme için gerektiği kadar ve farklı ad sembolleri ile tümel özelleme yapılabilir
Yol üzerinde hem bir tikel önerme hem de bir tümel önerme geçiyorsa tikel özellemenin daha önce yapılması tercih edilir.
Tümel özelleme yapılırken çelişki oluşturabilecek özellemelere öncelik verilir.
Örnek12.2
∀x (F(xc) →G(xb)), F(ac) ∧ ¬G(a,b) önermelerinin çözümleyici çizelgesi
Ayrıca önemli değişiklik de Tamamlanmış Açık Yol tanımındadır. Önermeler mantığında temel önerme olmayan çözümlenmemiş hiçbir önerme içermeyen açık yolları tamamlanmış açık yol olarak tanımlamıştır. Niceleme mantığında ise şu şekilde tanımlanır:
[Tamamlanmış Açık Yol]{.underline}: Şu 3 şartı sağlayan yol:
- Açık yol olan
- Çözümlenmemiş hiçbir önerme içermeyen
- Üzerindeki tümel önermeler yolun üzerindeki her ad sembolü için özellenmiş olan.
Örnek12.3
∀x(F(x) ∧ ¬G(x)), ¬F(a) ∨ G(b) önermelerinin çözümleyici çizelgesi
[Tikel Niceleyinin Değilleme Kuralı ( ¬∃)]{.underline}
¬ ∃xP
∀x ¬P (sıra numarası, ¬∃)
[Tümel Niceleyicinin Değilleme Kuralı (\ ¬∀)]{.underline}
¬ ∀xP
∃x ¬P (sıra numarası, ¬∀)
Örnek12.4
¬ ∀x(F(x) →G(x)), ∀x(F(x)↔︎G(x)) önermelerinin çözümleyici çizelgesi
Örnek12.5
∃x(G(x) →F(xb)), ¬ ∃xF(xb) önermelerinin çözümleyici çizelgesi
