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