snippets of logic - propositional logic

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^*