Éditeur de formules
Rédigez librement. Les raccourcis texte sont convertis à la frappe ; la palette insère à la position du curseur.
Raccourcis clavier
Valables dans tous les champs de tous les modules. La conversion a lieu dès que la séquence est complète. Les séquences \lnot, \land, \forall… sont les commandes LaTeX, les mêmes que celles produites par l'export LaTeX.
Export LaTeX
Chaque ligne est placée entre $ … $ ; les symboles deviennent \lnot, \land, \lor, \rightarrow, \leftrightarrow, \oplus, \top, \bot, \forall, \exists, \equiv, \vdash, \models, \in, \notin, \subseteq ; les indices P₁₂ deviennent P_{12}.
Export Markdown
Le texte est conservé tel quel (les symboles Unicode sont valides en Markdown) ; chaque retour à la ligne est rendu par un saut de ligne forcé (deux espaces en fin de ligne).
Table de vérité automatique
Variables : lettres majuscules, éventuellement indicées (P, Q₁, R2). Priorité : ¬ > ∧ > ∨, ⊕ > → > ↔ ; → est associatif à droite. Constantes ⊤ et ⊥ acceptées. Au plus 8 variables.
Table manuelle
Grille éditable : modifiez les en-têtes, tapez V ou F dans les cellules (v, 1, t → V ; f, 0 → F ; autre → vide). Ajoutez lignes et colonnes selon vos besoins.
Arbres : tableaux sémantiques et arbres de vérité
Sélectionnez un nœud dans la liste (ou dans le dessin) puis agissez avec les boutons. Plusieurs formules dans un même nœud : séparez-les par « ; ». Entrée dans un nœud ajoute un frère (un fils pour la racine).
Nœuds
Rendu
Déduction naturelle
Chaque ligne porte une formule, une justification (règle), les lignes référencées et un niveau d'hypothèse. Ouvrir une sous-preuve crée une ligne d'hypothèse indentée ; la fermer revient au niveau précédent. Entrée dans une formule ajoute une ligne en dessous.
| N° | Formule | Justification | Lignes | Niv. |
|---|
Générateur d'exercices
Choisissez un type et un niveau, puis cliquez sur « Nouvel exercice ».