8. Elsőrendű logika - Laptörténet

Gerbazse, 2013. november 4., 20:45-n

2013-11-04T20:45:08Z

← Régebbi változat		A lap 2013. november 4., 22:45-kori változata
117. sor:		117. sor:
	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		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		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]
	<math> \lor </math> már igaz volt és nem volt olyan cselekvés, ami hamissá tette volna]

	===8.7. A világ rejtett tulajdonságai===		===8.7. A világ rejtett tulajdonságai===

Gerbazse: Felsorolás helyrerakva

2013-11-04T20:40:50Z

Felsorolás helyrerakva

← Régebbi változat		A lap 2013. november 4., 22:40-kori változata
90. sor:		90. sor:
	# 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)		# 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)
	# Egzisztenciális kvantorokat eltüntetni.		# Egzisztenciális kvantorokat eltüntetni.
	** Skolemizálás (egzisztenciális kvantorok eliminálási folyamata)		#* 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)		#** <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).		#** 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> <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(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		#** <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
	# 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)		# 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)
	# Univerzális kvantorokat balra kihelyezni. ....<math> \forall </math>x....<math> \forall </math>y.. = <math> \forall </math>x<math> \forall </math>y ....x...y..		# Univerzális kvantorokat balra kihelyezni. ....<math> \forall </math>x....<math> \forall </math>y.. = <math> \forall </math>x<math> \forall </math>y ....x...y..

Gerbazse: LaTeX képletek javítva

2013-11-04T18:40:42Z

LaTeX képletek javítva

← Régebbi változat		A lap 2013. november 4., 20:40-kori változata
45. sor:		45. sor:
	'''Univerzális kvantor eliminálása:'''		'''Univerzális kvantor eliminálása:'''
	<math>		<math>
	$\frac{\forall x P(x, A)}{P(B, A)}$</math>		\frac{\forall x P(x, A)}{P(B, A)}</math>

	'''Egzisztenciális kvantor eliminálása:'''		'''Egzisztenciális kvantor eliminálása:'''
	<math>$\frac{\exists x Q(x, A)}{Q(B,A)}$</math>		<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.		, 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:'''		'''Egzisztenciális kvantor bevezetése:'''
	<math>$\frac{P(B,A)}{\exists x P(x, A)} $</math>		<math>\frac{P(B,A)}{\exists x P(x, A)} </math>

	'''Rezolúció:'''		'''Rezolúció:'''

Unknown user: Új oldal, tartalma: „{{GlobalTemplate|Infoalap|MIOsszefoglaloElsorenduLogika}} TOC ==Általános tudnivalók, tételek, definíciók== A világot objektumok alkotják, amelyek mási…”

2012-10-21T20:05:28Z

Új oldal, tartalma: „{{GlobalTemplate|Infoalap|MIOsszefoglaloElsorenduLogika}} __TOC__ ==Általános tudnivalók, tételek, definíciók== A világot objektumok alkotják, amelyek mási…”

Új lap

{{GlobalTemplate|Infoalap|MIOsszefoglaloElsorenduLogika}}

__TOC__

==Á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. <br />
'''Pl.:''' <br />
''eredeti mondat:'' <math>\exists!</math> r Uralkodó(r, Freedonia) <math> \land \forall</math> s Uralkodó(s, Freedonia) <math>\Rightarrow</math> Halott(s) <br />
''ú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:'''
# Implikációt eltüntetni: A <math> \Rightarrow </math> B = ¬A <math> \lor </math> B
# 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)
# 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
# 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)
# Univerzális kvantorokat balra kihelyezni. ....<math> \forall </math>x....<math> \forall </math>y.. = <math> \forall </math>x<math> \forall </math>y ....x...y..
# 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
# Konjunkciókat eltüntetni. Bontás diszjunktív klózokra
# Ha szükséges, a változókat átnevezni.
# 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]

===8.7. A világ rejtett tulajdonságai===

===8.8. Választás cselekvések közt===

===8.9. Célorientált ágens felé===

===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.

==Kérdések:==

[[Category:Infoalap]]

8. Elsőrendű logika - Laptörténet

Gerbazse, 2013. november 4., 20:45-n

Gerbazse: Felsorolás helyrerakva

Gerbazse: LaTeX képletek javítva

Unknown user: Új oldal, tartalma: „{{GlobalTemplate|Infoalap|MIOsszefoglaloElsorenduLogika}} __TOC__ ==Általános tudnivalók, tételek, definíciók== A világot objektumok alkotják, amelyek mási…”

Unknown user: Új oldal, tartalma: „{{GlobalTemplate|Infoalap|MIOsszefoglaloElsorenduLogika}} TOC ==Általános tudnivalók, tételek, definíciók== A világot objektumok alkotják, amelyek mási…”