∀ 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 σ
σ
=
{
E
}
mit
dem 2-stelligen Relationssymbol
E
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
∀
z
(
(
E
(
x
,
y
)
∧
E
(
y
,
z
)
)
→
E
(
x
,
z
)
)
Variablenmengen der Formel
Menge der Variablen:
{
x
,
y
,
z
}
Menge der freien Variablen:
{
}
Menge der gebundenen Variablen:
{
z
,
y
,
x
}
Test auf Normalformen
∀
x
∀
y
∀
z
(
(
E
(
x
,
y
)
∧
E
(
y
,
z
)
)
→
E
(
x
,
z
)
)
ist nicht in Negationsnormalform.
*
∀
x
∀
y
∀
z
(
(
E
(
x
,
y
)
∧
E
(
y
,
z
)
)
→
E
(
x
,
z
)
)
ist in Pränex.
*
Additional functions
Negationsnormalform berechenen
*
Pränex - Normalform berechenen
*
Syntaxbaum der Formel angeben
*