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)`
  • `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)