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

Parsen der Eingabe als Klausel(menge)^*

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

Definiere Formel φ entsprechend der Eingabe^*

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

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 :

A, B.

Check for normal forms (nnf, cnf, dnf)

Formula is in negation normal form.
Formula is not in disjunctive normal form.
Formula is in conjunctive normal form.

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