∀ 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 σ
σ
=
{
R_1
,
R_2
,
a
,
b
,
c
}
mit
dem 3-stelligen Relationssymbol
R_1
dem 1-stelligen Relationssymbol
R_2
den Konstantensymbolen:
a
b
c
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
(
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.
*
Additional functions
Negationsnormalform berechenen
*
Pränex - Normalform berechenen
*
Syntaxbaum der Formel angeben
*
