¬ x (x ∧ y) (x ↔ y) {A,¬B} {{A,¬B},{A,B}}
roadmap about config

Input

(show/hide hints for input)
Formel valid inputs
¬ y ~ y (by tilde)
  or alternatively
!y or &n y
( x ∧ y ) (x /\ y) (by slash and backslash)
  or alternatively
(x && y) or (x &w y )
( x ∨ y ) (x \/ y) (by backslash and slash)
  or alternatively
(x || y) or (x &v y )
( x → y ) (x -> y)
  or alternatively
(x &r y )
( x ↔ y ) (x <-> y)
  or alternatively
(x &l y )
1 1
  or alternatively
&1
0 0
  or alternatively
&0

Ihre Eingabe*

Definiere Formel φ entsprechend der Eingabe*

φ = (x↔y)

Ergebnis Syntaxcheck für Formel* φ

Syntax check quietverbosevery verbose

Syntactically correct propositional formula!

List of propositional variables in the formula φ

2 propositional variable(s) found, in fact :

x, y.

Check for normal forms (nnf, cnf, dnf)

Formula is not in negation normal form.
Und deshalb auch nicht in disjuntiver oder konjunktiver Normalform.*

Weitere Funktionen aufrufen

Auswerten der Formel φ unter vorgegebener Interpretation*
Draw the syntax tree
Truth table
Liste der erfüllenden Interpretationen*
Dual formula
Disjunctive normal form (erzeugt aus erfüllenden Interpretationen*)
Conjunctive normal form (erzeugt aus nicht erfüllenden Interpretationen*)
Negation normal form
Tseitin-Verfahren*
Resolutionswiderlegung*
Resolutionsalgorithmus*
DPLL-Algorithmus*
Hornklauseltest und ggf. Streichungsalgorithmus*

* translation not available