∀ 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 config

Signatur σ

σ={R_1,R_2,a,b,c}   mit
dem 3-stelligen Relationssymbol R_1
dem 1-stelligen Relationssymbol R_2
den Konstantensymbolen: abc

Signatur festlegen*

Formel/Term-Eingabe

Hinweise zur Formeleingabe finden Sie hier.

   
  Syntaxcheck:  calmeverbeuxtrès verbeux
  Signatur:  festhalten*erweitern*neu erstellen*

Ergebnis Syntaxcheck (Formel)

Syntaktisch korrekte FO[σ]-Formel!

Eingabe entspricht der Formel

(R_1(a,b,c)R_2 (a))

Variablenmengen der Formel

Menge der Variablen: {a}
Menge der freien Variablen: {a}
Menge der gebundenen Variablen: {}

Test auf Normalformen

(R_1(a,b,c)R_2 (a)) ist in Negationsnormalform.*
(R_1(a,b,c)R_2 (a)) ist quantorenfrei und daher in Pränex.*

Fonctions supplémentaires

Negationsnormalform berechenen*
Pränex - Normalform berechenen*
Syntaxbaum der Formel angeben*