Formelsammlung Aussagenlogik, Prädikatenlogik, Beschreibungslogik
DeMorgan
Seien im folgenden `o+` und `o.` Platzhalter für zwei unterschiedliche Zeichen aus der Zeichenmenge `{vv,^^}` . Lese das Zeichen "`-=`" als "lässt sich wahrheitserhaltend syntaktisch umformen in".
Dann gilt:
- `A o+ (B o. C) -= (Ao+B)o.(Ao+C)`
- ausgeschrieben:
- `A vv (B ^^ C) -= (A vv B) ^^ (A vv C)`
- `A ^^ (B vv C) -= (A ^^ B) vv (A ^^ C)`
- ausgeschrieben:
- `not (Ao+B) -= not A o. not B`
- `not AA x [F(x)] -= EE x [ not F(x)]`
- `not EE x [F(x)] -= AA x [ not F(x)]`
Austauschen der Reihenfolge von Quantoren:
- `AA x [ AA y [ F(x,y)]] -= AA y [ AA x [ F(x,y)]] `
- `EE x [ EE y [ F(x,y)]] -= EE y [ EE x [ F(x,y)]] `
- `EE x [ AA y [ F(x,y)]] -= AA y [ EE x [ F(x,y)]] `
- es gilt jedoch NICHT:
- `AA x [ EE y [ F(x,y)]] -= EE y [ AA x [ F(x,y)]] ` FALSCH
Skolemisierung ("von innen nach außen"):
- `AA x EE y AA z EE w F(x,y,z,w)`
- `~= AA x EE y AA z F(x,y,z,f(x,y,z))`
- `~= AA x AA z F(x,g(x),z,f(x,g(x),z))`
Zusammenfassen von Formeln:
- `AA x [ G(x) ] ^^ AA x [ H(x)] -= AA x [ G(x) ^^ H(x)] `
- `EE x [ G(x) ] vv EE x [ H(x)] -= EE x [ G(x) vv H(x)] `
- es gilt jedoch NICHT:
- `AA x [ G(x) ] vv AA x [ H(x)] -= AA x [ G(x) vv H(x)] ` FALSCH
- `EE x [ G(x) ] ^^ EE x [ H(x)] -= EE x [ G(x) ^^ H(x)] ` FALSCH
- in diesen Fällen kann eine neue Variable eingeführt werden:
- `AA x [ G(x) ] vv AA x [ H(x)] -= AA x AA y [ G(x) vv H(y)] `
- `EE x [ G(x) ] ^^ EE x [ H(x)] -= EE x EE y [ G(x) ^^ H(y)] `
Vertiefung: de.wikipedia.org > Wiki > De Morgansche Gesetze
Übersetzung von OWL-Primitiven nach FOL
( Je nach Laune kann man die folgenden Prädikate lesen als `"Nass"`, `"Kalt"`, `"Glatt"` oder `"Gruselig"`.)`G supe N ^^ K`
- in FOL: `AA x [ G(x) larr N(x) ^^ K(x) ]`
- Normalisierung:
- `G larr N ^^ K`
- `G vv not (N ^^ K)` (DNF)
- `G vv not N vv not K` (KNF und Horn)
`N ^^ K supe G`
- in FOL: `AA x [ N(x) ^^ K(x) larr G(x)]`
- Normalisierung:
- `N ^^ K larr G`
- `(N ^^ K) vv not G`
- `(N vv not G) ^^ (K vv not G)` (KNF und Horn)
- Hinweis: Ein `und` im Kopf einer Regel kann durch Lloyd-Topor-Transformation in zwei
einzelne Regeln aufgesplittet werden. Man erhält dann sofort
- `(N larr G) ^^ (K larr G)` (KNF, Horn)
`G supe N vv K`
- in FOL: `AA x [ G(x) larr N(x) vv K(x) ]`
- Normalisierung:
- `G larr N vv K`
- `G vv not (N vv K)` (DNF)
- `G vv (not N ^^ not K)`
- `(G vv not N) ^^ (G vv not K)` (KNF, Horn)
`N vv K supe G`
- in FOL: `AA x [ N(x) vv K(x) larr G(x)]`
- Normalisierung:
- `N vv K larr G`
- `(N vv K) vv not G`
- `(N vv K vv not G)` (KNF, nicht Horn)
- Hinweis: Ein `oder` im Kopf einer FLO-Regel ist nicht erlaubt. Wie man dennoch einen
kleinen Schritt weiterkommt:
- Führe eine neues Prädikat `m` ein, mit `M larr N` und `M larr K`
- Ersetze `N vv K supe G` durch `M supe G`
`AA P.C`
- in FOL: `AA x,y [ P(x,y) rarr C(y)]`
- Normalisierung:
- `P(x,y) rarr C(y)`
- `C(y) vv not P(x,y)` (KNF, Horn)
`EE P.C`
- in FOL: `AA x EE y [ P(x,y) ^^ C(y)]`
- Normalisierung: Eliminierung des Existenzquantors durch Skolemisierung: Ergebnis der
Umformung ist lediglich erfüllbarkeitsäquivalent!
- `P(x,f(x)) ^^ C(f(x))` (KNF, Horn)