Az informatikai logikai alapjai
Az elsőrendű matematikai logikai nyelv
A nyelv interpretációja
Formulák igazságértéke az interpretációban adott változókiértékelés mellett
Logikai törvény
Logikai következmény
Logikai ekvivalencia
Normálformák
Kalkulusok (Gentzen-kalkulus)
<Srt, Pr, Fn, Cnst>
Srt - fajták
Pr - predikátumszimbólumok
Fn - függvényszimbólumok
Cnst - konstansszimbólumok
ábécéje
logikai összekötőjelek
kvantorok
különböző fajtájú változók
negáció
konjunkció
diszjunkció
implikáció
egzisztenciális
univerzális
elválasztójelek
term
formula
változó
konstans
függvényszimbólum
atomi formula
kvantált formula
közvetlen részterm
közvetlen részformula
funkcionális összetettség
logikai összetettség
változó, konstants - 0
függvényszimbólum esetén a paraméterek termek szummája
predikátumszimbólum
atomi formula - 0
negáció, konjunkció, diszjunkció, implikáció, kvantorok - részformula összetettség + 1
változó előfordulás
szabad
kötött
kvantor köti
változó átnevezés
a változó minden szabad előfordulását cseréljük
kongruencia
I(Srt)
I(Pr)
I(Fn)
I(Cnst)
függvény ami minden fajtához megadja az individumok halmazát, ezeknek a halmazoknak az unióját nevezzük az interpretáció univerzumának
függvény ami minden predikátumszimbólumhoz egy logikai függvényt rendel
függvény ami minden függvényszimbólumhoz hozzárendel egy matematikai függvényt
függvény ami minden konstansszimbólumhoz egy individumot rendel
változókiérteklés
kielégíthető
kielégíthetetlen
minden interpretációban és változókiértékelés mellett az igazságérték megegyezik
prenex alak
változóiban tiszta formula
elérésének lépései
változó-tiszta alakra hozni a formulát
kvantorkiemeléses szabályokat alkalmazzuk
Egy formula logikai következménye egy formulahalmaznak ha minden olyan interpretációja és változókiértékelése amely kielégít minden a formulahalmazban levő formulát, az kielégíti az eredeti formulát is.
konjunktív normálforma
diszjunktív normálforma
szekvent
axiómasémák
levezetési szabályok