¬ 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
Tseitin-Verfahren
Resolutionswiderlegung
Resolutionsalgorithmus
DPLL-Algorithmus
Hornklauseltest und ggf. Streichungsalgorithmus