¬ x (x ∧ y) (x ↔ y) {A,¬B} {{A,¬B},{A,B}}
Roadmap Über config

Eingabe

(Hinweise zur Eingabe an/ausschalten)
Formel zulässige Eingaben
¬ y ~ y (mittels Tilde)
  oder alternativ
!y oder &n y
( x ∧ y ) (x /\ y) (mittels Slash und Backslash)
  oder alternativ
(x && y) oder (x &w y )
( x ∨ y ) (x \/ y) (mittels Backslash und Slash)
  oder alternativ
(x || y) oder (x &v y )
( x → y ) (x -> y)
  oder alternativ
(x &r y )
( x ↔ y ) (x <-> y)
  oder alternativ
(x &l y )
1 1
  oder alternativ
&1
0 0
  oder alternativ
&0

Ihre Eingabe

Parsen der Eingabe als Klausel(menge)

ΓDisjKl ={{A,¬B},{A,B}}

Definiere Formel φ entsprechend der Eingabe

φ = ((A∨¬B)∧(A∨B))

Ergebnis Syntaxcheck für Formel φ

Syntaxcheck stillgeschwätzigsehr geschwätzig

Syntaktisch korrekte aussagenlogische Formel!

Liste der aussagenlogischen Variablen in der Formel φ

2 aussagenlogische Variable(n) gefunden, und zwar :

A, B.

Test auf Normalformen (NNF, DNF, KNF)

Formel ist in Negationsnormalform.
Formel ist nicht in disjunktiver Normalform.
Formel ist in konjunktiver Normalform.

Weitere Funktionen aufrufen

Auswerten der Formel φ unter vorgegebener Interpretation
Syntaxbaum zeichnen
Wahrheitstafel
Liste der erfüllenden Interpretationen
Angabe der dualen Formel
Disjunktive Normalform (erzeugt aus erfüllenden Interpretationen)
Konjunktive Normalform (erzeugt aus nicht erfüllenden Interpretationen)
Negationsnormalform
Resolutionswiderlegung
Resolutionsalgorithmus
DPLL-Algorithmus
Hornklauseltest und ggf. Streichungsalgorithmus