∀ 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 σ
∅
Signatur festlegen
*
Formel/Term-Eingabe
Hinweise zur Formeleingabe finden Sie
hier
.
Syntaxcheck:
quiet
verbose
very verbose
Signatur:
festhalten
*
erweitern
*
neu erstellen
*
Ergebnis Syntaxcheck (Formel)
Syntaktisch korrekte FO[σ]-Formel!
Eingabe entspricht der Formel
∀
x
∃
y
x
=
y
Variablenmengen der Formel
Menge der Variablen:
{
x
,
y
}
Menge der freien Variablen:
{
}
Menge der gebundenen Variablen:
{
y
,
x
}
Test auf Normalformen
∀
x
∃
y
x
=
y
ist in Negationsnormalform.
*
∀
x
∃
y
x
=
y
ist in Pränex.
*
Additional functions
Negationsnormalform berechenen
*
Pränex - Normalform berechenen
*
Syntaxbaum der Formel angeben
*
