Önermeli ve birinci dereceden mantık-temelli modeller

Afshine Amidi ve Shervine Amidi tarafından

Ayyüce Kızrak ve Başak Buluz tarafından çevrilmiştir

Temeller

Önerme mantığının sözdizimi $f$ , $g$ formülleri ve $\neg, \wedge, \vee, \rightarrow, \leftrightarrow$ bağlayıcılarını belirterek, aşağıdaki mantıksal ifadeleri yazabiliriz:

Adı	Sembol	Anlamı	Gösterim
Doğrulama	$f$	$f$
Dışlayan	$\neg f$	$f$ değil
Kesişim	$f\wedge g$	$f$ ve $g$
Birleşim	$f\vee g$	$f$ veya $g$
Implication	$f\rightarrow g$	eğer $f$ 'den $g$ çıkarsa
İki koşullu	$f\leftrightarrow g$	$f$ ve $g$ 'nin ortak olduğu bölge

Not: bu bağlantılar dışında tekrarlayan formüller oluşturulabilir.

Model $w$ modeli, ikili sembollerin önermeli sembollere atanmasını belirtir.

Örnek: $w = \{A:0, B:1, C:0\}$ doğruluk değerleri kümesi, $A$ , $B$ ve $C$ önermeli semboller için olası bir modeldir.

Yorumlama fonksiyonu Yorumlama fonksiyonu $\mathcal{I}(f,w)$ , $w$ modelinin $f$ formülüne uygun olup olmadığını gösterir:

\boxed{\mathcal{I}(f,w)\in\{0,1\}}

Modellerin seti $\mathcal{M}(f)$ , $f$ formülünü sağlayan model setini belirtir. Matematiksel konuşursak, şöyle tanımlarız:

\boxed{\mathcal{M}(f) = \{w\, |\, \mathcal{I}(f,w)=1\}}

Bilgi temelli

Tanım Bilgi temeli $\textrm{KB}$ (knowledge base), şu ana kadar düşünülen tüm formüllerin birleşimidir. Bilgi temelinin model kümesi, her formülü karşılayan model dizisinin kesişimidir. Diğer bir deyişle:

\boxed{\mathcal{M}(\textrm{KB})=\bigcap_{f\in\textrm{KB}}\mathcal{M}(f)}

Olasılıksal yorumlama $f$ sorgusunun $1$ olarak değerlendirilmesi olasılığı, $f$ 'yi sağlayan bilgi temeli $\textrm{KB}$ 'nin $w$ modellerinin oranı olarak görülebilir, yani:

\boxed{P(f\,|\,\textrm{KB})=\frac{\displaystyle\sum_{w\in\mathcal{M}(\textrm{KB})\cap\mathcal{M}(f)}P(W=w)}{\displaystyle\sum_{w\in\mathcal{M}(\textrm{KB})}P(W=w)}}

Gerçeklenebilirlik En az bir modelin tüm kısıtlamaları yerine getirmesi durumunda $\textrm{KB}$ 'nin bilgi temelinin gerçeklenebilir olduğu söylenir. Diğer bir deyişle:

\boxed{\textrm{KB karşılanabilirlik}\Longleftrightarrow\mathcal{M}(\textrm{KB})\neq\varnothing}

Not: $\mathcal{M}(\textrm{KB})$ , bilgi temelinin tüm kısıtları ile uyumlu model kümesini belirtir.

Formüller ve bilgi temeli arasındaki ilişki Bilgi temeli $\textrm{KB}$ ile yeni bir formül $f$ arasında aşağıdaki özellikleri tanımlarız:

Adı	Matematiksel formülü	Gösterim	Notlar
$\textrm{KB}$ $f$ içerir	$\mathcal{M}(\textrm{KB})\cap\mathcal{M}(f)=\mathcal{M}(\textrm{KB})$		• $f$ yeni bir bilgi getirmiyor • Ayrıca $\textrm{KB}\models f$ yazıyor
$\textrm{KB}$ $f$ içermez	$\mathcal{M}(\textrm{KB})\cap\mathcal{M}(f)=\varnothing$		• Hiçbir model $f$ ekledikten sonra kısıtlamaları yerine getirmiyor • $\textrm{KB}\models\neg f$ 'ye eşdeğer
$f$ koşullu $\textrm{KB}$	$\mathcal{M}(\textrm{KB})\cap\mathcal{M}(f) \neq \varnothing$ ve $\mathcal{M}(\textrm{KB})\cap\mathcal{M}(f)\neq\mathcal{M}(\textrm{KB})$		• $f$ $\textrm{KB}$ 'ye aykırı değil • $f$ $\textrm{KB}$ 'ye önemsiz miktarda bilgi ekliyor

Model denetimi Bir model denetimi algoritması, $\textrm{KB}$ 'nin bilgi temelini girdi olarak alır ve bunun karşılanabilir olup olmadığını çıkarır.

Not: popüler model kontrol algoritmaları DPLL ve WalkSat'ı içerir.

Çıkarım kuralı $f_1,...,f_k$ ve sonuç $g$ yapısının çıkarım kuralı şöyle yazılmıştır:

\boxed{\frac{f_1,...,f_k}{g}}

İleri çıkarım algoritması Çıkarım kurallarından $\textrm{Rules}$ , bu algoritma mümkün olan tüm $f_1, ..., f_k$ 'den geçer ve eşleşen bir kural varsa, $\textrm{KB}$ bilgi tabanına $g$ ekler. Bu işlem $\textrm{KB}$ 'ye daha fazla ekleme yapılamayana kadar tekrar edilir.

Türetme $f$ 'nin $\textrm{KB}$ içerisindeyse veya $\textrm{Rules}$ kurallarını kullanarak ileri çıkarım algoritması sırasında eklenmişse, $\textrm{KB}$ 'nin $\textrm{Rules}$ ile $f$ ( $\textrm{KB}\vdash f$ yazılır) türettiğini söylüyoruz.

Çıkarım kurallarının özellikleri Çıkarım kurallarının kümesi $\textrm{Rules}$ aşağıdaki özelliklere sahip olabilir:

Adı	Matematiksel formülü	Notlar
Sağlamlık	$\{f \, \| \, \textrm{KB}\vdash f\}\subseteq\{f \, \| \, \textrm{KB}\models f\}$	• Çıkarılan formüller $\textrm{KB}$ arafından sağlanmıştır • Her defasında bir kural kontrol edilebilir • "Gerçeğinden başka bir şey yok"
Tamlık	$\{f \, \| \, \textrm{KB}\vdash f\}\supseteq\{f \, \| \, \textrm{KB}\models f\}$	• Ya $\textrm{KB}$ 'yi içeren formüller ya bilgi tabanında zaten vardır, ya da ondan çıkarılan değerlerdir • "Tüm gerçek"

Önerme mantığı

Bu bölümde, mantıksal formülleri ve çıkarım kurallarını kullanan mantık tabanlı modelleri inceleyeceğiz. Buradaki fikir ifade ve hesaplamanın verimliliğini dengelemektir.

Horn cümlesi $p_1,...,p_k$ ve $q$ önerme sembollerini not ederek, bir Horn cümlesi şu şekildedir (matematiksel mantık ve mantık programlamada, kural gibi özel bir biçime sahip mantıksal formüllere Horn cümlesi denir):

\boxed{(p_1\wedge...\wedge p_k)\longrightarrow q}

Not: $q=\textrm{False}$ olduğunda, "hedeflenen bir cümle" olarak adlandırılır, aksi takdirde "kesin bir cümle" olarak adlandırırız.

Modus ponens $f_1,...,f_k$ ve $p$ önermeli semboller için modus ponens kuralı yazılır:

\boxed{\frac{f_1,...,f_k,\quad (f_1\wedge...\wedge f_k)\longrightarrow p}{p}}

Not: her uygulama tek bir önermeli sembol içeren bir cümle oluşturduğundan, bu kuralın uygulanması doğrusal bir zaman alır.

Tamlık $\textrm{KB}$ 'nin sadece Horn cümleleri içerdiğini ve $p$ 'nin zorunlu bir teklif sembolü olduğunu varsayalım, Hornus cümlelerine göre modus ponenleri tamamlanmıştır. Modus ponens uygulanması daha sonra $p$ 'yi türetir.

Konjunktif normal form Bir konjonktif normal form (CNF, conjunctive normal form) formülü, her bir cümlenin atomik formüllerin bir ayrıntısı olduğu cümle birleşimidir.

Açıklama: başka bir deyişle, CNF'ler $\vee$ ait $\wedge$ bulunmaktadır.

Eşdeğer temsil Önerme mantığındaki her formül eşdeğer bir CNF formülüne yazılabilir. Aşağıdaki tabloda genel dönüşüm özellikleri gösterilmektedir:

Kural adı		Başlangıç	Dönüştürülmüş
Eleme	$\leftrightarrow$	$f \leftrightarrow g$	$(f \rightarrow g) \wedge (g \rightarrow f)$
	$\rightarrow$	$f \rightarrow g$	$\neg f \vee g$
	$\neg\neg$	$\neg\neg f$	$f$
Dağıtma	$\neg$ üzerine $\wedge$	$\neg(f \wedge g)$	$\neg f \vee \neg g$
	$\neg$ üzerine $\vee$	$\neg(f \vee g)$	$\neg f\wedge \neg g$
	$\vee$ üzerine $\wedge$	$f \vee (g \wedge h)$	$(f \vee g) \wedge (f \vee h)$

Çözünürlük kuralı $f_1,...,f_n$ ve $g_1,...,g_m$ önerme sembolleri için, $p$ , çözümleme kuralı yazılır:

\boxed{\frac{f_1\vee...\vee f_n\vee p,\quad\neg p\vee g_1\vee...\vee g_m}{f_1\vee...\vee f_n\vee g_1\vee...\vee g_m}}

Not: her uygulama, teklif sembollerinin alt kümesine sahip bir cümle oluşturduğundan, bu kuralı uygulamak için üssel olarak zaman alabilir.

Çözünürlük tabanlı çıkarım Çözünürlük tabanlı çıkarım algoritması, aşağıdaki adımları izler:

Adım 1: Tüm formülleri CNF'ye dönüştürün
Adım 2: Tekrar tekrar, çözünürlük kuralını uygulayın
Adım 3: $\text{False}$ türetilmişse tatmin edici olmayan dönüş yapın

Birinci dereceden mantık

Buradaki fikir, daha kompakt bilgi sunumları sağlamak için değişkenleri kullanmaktır.

Model Birinci mertebeden mantık haritalarında bir $w$ modeli:

nesnelere sabit semboller
nesnelerin dizisini sembolize etmek için tahmin

Horn cümlesi $x_1,...,x_n$ değişkenleri ve $a_1,...,a_k,b$ atomik formüllerine dikkat çekerek, bir boynuz maddesinin birinci derece mantık versiyonu aşağıdaki şekildedir:

\boxed{\forall x_1,...,\forall x_n,\quad(a_1\wedge...\wedge a_k)\rightarrow b}

Yer değiştirme Bir yerdeğiştirme değişkenleri terimlerle eşler ve $\textrm{Subst}[\theta,f]$ yerdeğiştirme sonucunu $f$ olarak belirtir.

Birleştirme Birleştirme $f$ ve $g$ 'nin iki formülünü alır ve onları eşit yapan en genel ikameyi $\theta$ verir:

\boxed{\textrm{Unify}[f,g]=\theta}\quad\textrm{ öyle ki }\quad\boxed{\textrm{Subst}[\theta,f]=\textrm{Subst}[\theta,g]}

Not: $\textrm{Unify}[f,g]$ eğer böyle bir $\theta$ yoksa $\textrm{Fail}$ döndürür.

Modus ponens $x_1,...,x_n$ değişkenleri, $a_1, ..., a_k$ ve $a'_1,...,a'_k$ atomik formüllerine dikkat ederek ve $\theta = \textrm{Unify}(a'_1\wedge ...\wedge a'_k, a_1\wedge ...\wedge a_k)$ modus ponenlerin birinci dereceden mantık versiyonu yazılabilir:

\boxed{\frac{a'_1,...,a'_k\quad\forall x_1,...,\forall x_n (a_1\wedge...\wedge a_k)\rightarrow b}{\textrm{Subst}[\theta, b]}}

Tamlık Modus ponens sadece Horn cümleleriyle birinci dereceden mantık için tamamlanmıştır.

Çözünürlük kuralı $f_1, ..., f_n$ , $g_1, ..., g_m$ , $p$ , $q$ formüllerini not ederek ve $\theta=\textrm{Unify}(p,q)$ ifadesini kullanarak, çözümleme kuralının birinci dereceden mantık sürümü yazılabilir:

\boxed{\frac{f_1\vee...\vee f_n\vee p,\quad\neg q\vee g_1\vee...\vee g_m}{\textrm{Subst}[\theta,f_1\vee...\vee f_n\vee g_1\vee...\vee g_m]}}

Yarı-karar verilebilirlik Birinci dereceden mantık, sadece Horn cümleleriyle sınırlı olsa bile, yarı karar verilebilir eğer:

$\textrm{KB}\models f$ ise $f$ sonsuz zamanlıdır
$\textrm{KB}\not\models f$ ise sonsuz zamanlı olabilirliği gösteren algoritma yoktur