¬ x (x ∧ y) (x ↔ y) {A,¬B} {{A,¬B},{A,B}}
feuille de route sur config

Entrée

(conseils pour l'entrée)
Formel entrées valides
¬ y ~ y (tilde)
  ou bien
!y ou &n y
( x ∧ y ) (x /\ y) ( une barre oblique et une barre oblique inverse)
  ou bien
(x && y) ou (x &w y )
( x ∨ y ) (x \/ y) ( une barre oblique inverse et une barre oblique)
  ou bien
(x || y) ou (x &v y )
( x → y ) (x -> y)
  ou bien
(x &r y )
( x ↔ y ) (x <-> y)
  ou bien
(x &l y )
1 1
  ou bien
&1
0 0
  ou bien
&0

Ihre Eingabe*

Definiere Formel φ entsprechend der Eingabe*

φ = ¬x

Ergebnis Syntaxcheck für Formel* φ

Vérification de la syntaxe calmeverbeuxtrès verbeux

La formule propositionnelle est syntaxiquement correcte!

Liste des variables propositionnelles de la formule φ

1 variable(s) propositionnelle(s) trouvée(s), à savoir :

x.

Test pour forme normale

Formule est dans la forme normale négative.
Formule est dans la forme normale disjonctive.
Formule est dans la forme normale conjonctive.

Weitere Funktionen aufrufen

Auswerten der Formel φ unter vorgegebener Interpretation*
Dessiner l'arbre syntaxique
Table de vérité
Liste der erfüllenden Interpretationen*
Formula dual
Forme normale disjonctive (erzeugt aus erfüllenden Interpretationen*)
Forme normale conjonctive (erzeugt aus nicht erfüllenden Interpretationen*)
Forme normale négative
Tseitin-Verfahren*
Resolutionswiderlegung*
Resolutionsalgorithmus*
DPLL-Algorithmus*
Hornklauseltest und ggf. Streichungsalgorithmus*

* traduction non disponible