∀ x ∃ y x=y ∀ x ∀ y ∀ z ((E(x,y) ∧ E(y,z) ) → E(x,z)) ∀ x ∃ y (Geschwister (x,Vater(Mutter(y))) → Vorfahr(y,x)) (R_1(.a,.b,.c) ∨ R_2 (a))
Hinweise Roadmap Über

Signatur festlegen

Leere Signatur σ=    σGraph =E    σBsp. 6.11c =fc    σ =+0
  σBsp. 6.23 =GeschwisterVorfahrVaterMutter
Eigene: zu σ=E
    der Stelligkeit hinzufügen

Signatur σ

σ=E   mit
dem 2-stelligen Relationssymbol E

Formeleingabe

Hinweise zur Formeleingabe finden Sie hier.

 
  Syntaxcheck still geschwätzig sehr geschwätzig
  Signatur festhalten erweitern neu erstellen

Ergebnis Syntaxcheck

Syntaktisch korrekte FO[σ]-Formel!

Eingabe entspricht der Formel

x y z ExyEyzExz

Variablenmengen der Formel

Menge der Variablen: xyz
Menge der freien Variablen:
Menge der gebundenen Variablen: zyx

Test auf Normalformen

x y z ExyEyzExz ist nicht in Negationsnormalform.
x y z ExyEyzExz ist in Pränex.

Weitere Funktionen aufrufen

Negationsnormalform berechenen
Pränex - Normalform berechenen