8. Elsőrendű logika

Ez az oldal a korábbi SCH wiki-ről lett áthozva. Az eredeti változata itt érhető el.

Ha úgy érzed, hogy bármilyen formázási vagy tartalmi probléma van vele, akkor kérlek javíts rajta egy rövid szerkesztéssel.

Ha nem tudod, hogyan indulj el, olvasd el a migrálási útmutatót

Általános tudnivalók, tételek, definíciók

A világot objektumok alkotják, amelyek másik objektumoktól megkülönböztető saját azonosítókkal és tulajdonságokkal rendelkező dolgok. Ezen objektumok között különböző relációk létezhetnek. A relációk közül néhány függvény )olyan reláció, ahol csak egy 'értéke' van egy adott'bemenet' esetén).

8.1. Szintaxis és szemantika

A mondatok (melyek tényeket reprezentálnak) mellett termjei is vannak, amik viszont az objektumokat reprezentálják.

• konstans szimbólum: specifikálják, hogy a világ mely objektumához tartoznak, minden ~ megnevez egy objektumot, de létezik névtelen, vagy több névvel rendelkező objektum is
• predikátum szimbólum: relációhoz köti az interpretáció, minden modellben a relációt az azt kielégítő objektum n-esek definiálják
• függvény szimbólum: néhány reláció függvény is egyben, amennyiben minden a relációban szereplő objektum pontosan egy objektummal van kapcsolatban

• Termek*: BalLába(Apja(János)), ...; egy term egy objektumra vonatkozó logikai kifejezés (konstans szimbólumok, tehát a legegyszerűbb termek), a változó nélküli termek az alaptermek.
• *atomi mondatok*: Bátyja(Apja(János)), Házas(Apja(Richárd), Anyja(János)), ...; tényeket fejeznek ki. egy atomi mondatot egy predikátum szimbólum, és az őt követő zárójelezett listán található termek listája alkotja. Az atomi mondatoknak lehetnek összetett termek is az argumentumai.
• *összetett mondatok*: pl.: Bátyja(Béla, Apja(János)) [math] \Rightarrow [/math] Házas(Apja(Richárd), Anyja(János)), használhatunk logikai összekötő szimbólumokkal még összetettebb mondatok építésére; az ~ igaz, ha a reláció, amire a predikátum szimbólum vonatkoozik, fennáll az argumentumok által jelölt objektumok között, természetesen ez a világ interpretációjától
• *kvantorok*: tulajdonságok, amelyek objektumok egész gyűjteményeire vonatkoznak, ahelyett hogy megneveznénk minden objektumot a nevével. Az elsőrendű logika két standard kvantort tartalmaz:
  • univerzális kvantor [math](\forall)[/math]: [math]\forall[/math] Macska(x) [math]\Rightarrow [/math] Emlős(x)
  • egzisztenciális kvantor [math](\exists)[/math]
  • egyediség kvantor [math](\exists!)[/math]: [math]\exists![/math] x Király(x), egyértelműen létezik egy egyedi objektum x, amely kielégíti a Király(x)-et - vagy kevésbé formálisan - létezik pontosan egy király

8.2. Bővítések

8.2.1. Magasabb rendű logikák

Megengedi az objektumokon értelmezett relációkat és függvényeket is, így nagyobb kifejezőereje van, mint az elsőrendű logikának.

8.2.2. A λ operátor

A λ kifejezés hasonló módon alkalmazható az argumentumokra egy logikai term létrehozásához, mint rendes, névvel rendelkező függvények esetében.

8.2.4. Az ι egyediségi operátor

Közvetlenül az egyedi objektum reprezentálására.
Pl.:
eredeti mondat: [math]\exists![/math] r Uralkodó(r, Freedonia) [math] \land \forall[/math] s Uralkodó(s, Freedonia) [math]\Rightarrow[/math] Halott(s)
új mondat: Halott(ι r Uralkodó(r, Freedonia))

8.3. Az elsőrendű logika használata

Modus Ponens: E1 P(A) E1 [math] \Rightarrow [/math] E2 [math] \forall [/math]x P(x) [math] \Rightarrow [/math] Q(x) (ilyen kvantifikált implikáció általában E2 Q(A) egy korábbi indukció eredménye)

Univerzális kvantor eliminálása: [math] \frac{\forall x P(x, A)}{P(B, A)}[/math]

Egzisztenciális kvantor eliminálása: [math]\frac{\exists x Q(x, A)}{Q(B,A)}[/math] , feltéve, hogy B-nek másutt nincs szerepe a tudásbázisban! B az ún. Skolem konstans, tehát bizonyos tulajdonságokkal rendelkező, pl. emberszerű, de a feladatban önálló léttel nem rendelkeő objektum.

Egzisztenciális kvantor bevezetése: [math]\frac{P(B,A)}{\exists x P(x, A)} [/math]

Rezolúció: [math]\begin{tabular}{l} $P(x, A) \lor Q(x)$ \\ $\neg Q(B) \lor R(x)$ \\ \hline $P(B, A) \lor R(b)$ \end{tabular}[/math]

Teljes: minden igaz állítás belátható (Gödel, 1930, egzisztenciális bizonyítás)

Félig eldönthető: hamis állítás hamis volta nem mutatható ki!

Általánosított Modus Ponens: ÉS bevezetése + Univerzális kvantor eliminálása + Modus Ponens ==> Általánosított Modus Ponens

[math] 
 \begin{tabular}{r}
 $P_1(x_1), P_2(x_2), \dots, P_n(x_n)$ \\
 $P_1(y_1) \land P_2(y_2) \land \dots P_n(y_n) \Rightarrow Q(y_1, y_2, \dots, y_n)$ \\
 \hline
$Q(x_1, x_2, \dots, x_n)$
\end{tabular}[/math]

Horn klózzá alakítás

Horn klóz: konjunkció [math] \Rightarrow [/math] egyetlen atom

Konverzió Horn-klózokká: egzisztenciális kvantor eliminálása + AND eliminálása

Modus Ponens lépés nem képes felhasználni a tudásbázis összes állítását, vagy a tudásbázis létrehozásánál mesterséges megkötéseket kell alkalmazni! (Modus Ponens alapú bizonyítás nem teljes, de az elsőrendű logika teljes)

Transzformáció klóz formára:

1. Implikációt eltüntetni: A [math] \Rightarrow [/math] B = ¬A [math] \lor [/math] B
2. Negálást az atomi formulák szintjére áthelyezni. ¬ (A [math] \lor [/math] B) = ¬A [math] \land [/math] ¬B, ¬[math] \forall [/math]x P(x) = [math] \exists [/math]x ¬P(x)
3. Egzisztenciális kvantorokat eltüntetni.
   • Skolemizálás (egzisztenciális kvantorok eliminálási folyamata)
     • [math] \exists [/math] x Owns(Nono, x)[math] \land [/math]Missile(x) ===> Owns(Nono, M1)
     • Missile(M1) Every person has a heart (Minden embernek van szíve).
     • [math] \forall [/math]x Person(x) [math] \Rightarrow [/math] [math] \exists [/math] y Heart(y) [math] \land [/math] Has(x, y)
     • [math] \forall [/math]x Person(x) [math] \Rightarrow [/math] Heart(H1)[math] \land [/math]Has(x, H1) feltéve, hogy H1 (egy fiktív szív) sehol sem szerepel a tudásbázisban
     • [math] \forall [/math]x Person(x) [math] \Rightarrow [/math] Heart(f(x)) [math] \land [/math]Has(x, f(x)) feltéve, hogy f(x) (minden x-hez egy fiktív szív) sehol sem szerepel a tudásbázisban
4. Ha szükséges, a változókat átnevezni. [math] \forall [/math]x P(x) [math] \lor [/math] [math] \forall [/math]x Q(x) ----------> [math] \forall [/math]x P(x) [math] \lor [/math] [math] \forall [/math]y Q(y)
5. Univerzális kvantorokat balra kihelyezni. ....[math] \forall [/math]x....[math] \forall [/math]y.. = [math] \forall [/math]x[math] \forall [/math]y ....x...y..
6. Diszjunkciókat literál szintjére áthelyezni. (A [math] \land [/math] B) [math] \lor [/math] C = (A [math] \lor [/math] C) [math] \land [/math] (B [math] \lor [/math] C), ami most megvan, az a konjunktív normal forma
7. Konjunkciókat eltüntetni. Bontás diszjunktív klózokra
8. Ha szükséges, a változókat átnevezni.
9. Univerzális kvantorokat elhagyni.

8.6. A világban történő változások reprezentálása

A szituáció kalkulus

A változások leírásának egy bizonyos módjának az elsőrendű logikában. Ez úgy tekinti a világot, hogy az szituációk sorozatából áll, amelynek mindegyike egy „pillanat felvétel” világ állapotáról.

Minden relációt vagy tulajdonságot amely időben változhat, a hozzátartozó predikátumhoz történő extra szituáció argumentum hozzáadása segítségével kezelünk. A szituáció argumentum mindig az utolsó és a szituáció konstansokat Si jelöli.

A hatás axióma szerepe leírni, hogy egy adott cselekvésnek milyen hatása van a világ általa megváltoztatott tulajdonságára.

A keret axiómák azt írják le, hogy hogyan marad a világ változatlan (a változás ellenkezőjeként). Együttesen a hatás axiómák és a keret axiómák egy teljes leírását adják, hogyan fejlődik a világ az ágens cselekvéseinek hatására.

Utód-állapot axióma: Összekombináljuk a hatás axiómákat és a keret axiómákat egyetlen axiómába, amely leírja hogyan számítsuk a Birtokol predikátumot a következő lépésben, ha adott az értéke a pillanatnyi lépésben. Egy ilyen axióma szükséges minden egyes predikátumhoz, amely változhat az idők során. Egy utód-állapot axiómának fel kell sorolnia, minden lehetséges módját a predikátum igazzá válásának és minden módot, amikor hamissá válik

Igaz utána [math] \Leftrightarrow [/math] [bármely cselekvés, amely igazzá tette [math] \lor [/math] már igaz volt és nem volt olyan cselekvés, ami hamissá tette volna]

Rezolúciós bizonyítás

Egy állítás ellentettjét hozzávesszük a konzisztens tudásbázishoz, meg rezolúcióval inkonzisztenciát keresünk. Ha a keletkezett tudásbázis inkonzisztens, akkor az eredeti állítás igaz.

Az inkonzisztencia keresésekor rezolúciós lépéseket hajtunk végre, amíg nem találunk triviális ellentmondást: p és nem p. A rezolúcióhoz a tudásbázist klóz formában kell tárolni. Az adott rezolúciós lépésben szereplő két klózt különböző stratégiákkal választhatjuk ki:

• Egységklóz preferencia: az egyik legyen szimpla literál
• Set of Support: a 'Set of Support' klózok halmaza, kezdetben a negált állítást tartalmazza. Mindig egy elemet váalsztunk a SoS-ből, és egyet a maradékból. Az eredmény a SoS-ba kerül. Ha a SoS-on kívüli klózok teljesíthetők, akkor az eljárás teljes.
• Input rezolúció: a negált állításhoz veszünk hozzá valakit, majd a következő lépésben az eredményhez veszünk hozzá valakit, stb. Horn-klóz alakú tudásbázisban az eljárás teljes, különben nem!
• Lineáris rezolúció: P és Q rezolválható, ha P benne van az eredeti tudásbázisban, vagy ha P a Q őse a bizonyítási fában. Lineáris rezolúció egy teljes eljárás.
• Egyszerűsítés: Elimináljunk minden olyan állítást, amely egy tudásbázisban létező állításnál specifikusabb.