∀ 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 σ=
    der Stelligkeit hinzufügen

Signatur σ

σ=   mit

Formeleingabe

Hinweise zur Formeleingabe finden Sie hier.

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

Variablenmengen der Formel

Menge der Variablen:
Menge der freien Variablen:
Menge der gebundenen Variablen:

Test auf Normalformen

internal Error: (sub)
ist in Negationsnormalform.
internal Error: (sub)
ist quantorenfrei und daher in Pränex.

Weitere Funktionen aufrufen

Negationsnormalform berechenen
Pränex - Normalform berechenen