On présente des outils simples pour l'enseignement de la
logique.
Ces logiciels sont mis à la
disposition de tous, avec l'appui du laboratoire
VERIMAG.
Γ ⊢ A ∨ B Γ, A ⊢ C Γ, B ⊢ C
----------------------------------- [∨E]
Γ ⊢ C
Ce logiciel fonctionne comme celui ci-dessus, la seule différence est la règle utilisée pour l'élimination de la disjonction.
Déduction naturelle propositionnelles avec la règle d'élimination ∨E et
les règles pour la négation et l'équivalence
Ce logiciel fonctionne comme celui ci-dessus.
Logiques modale, intuitioniste, GL par la méthode des Tabeaux
Logique du premier ordre
-
Preuve en logique du premier ordre par la résolution
Étant donnée une liste de clauses, ainsi que des limites sur le temps de la preuve et
la taille des clauses,
le logiciel tente de construire une preuve de la clause vide dans les limites imposées.
Le prouveur est complet : si l'ensemble des clauses est
insatisfaisable, et s'il n'y a pas de limite du temps de preuve et de la taille des clauses,
il en déduit la clause vide.
- La stratégie "prover9" en logique du premier ordre
Nous avons deux listes de clauses, l'une est la liste du support et l'autre est la liste utilisable.
A partir de ces deux listes, le logiciel tente de construire une preuve de la clause vide
dans les limites imposées.
Le prouveur est complet : si la liste utilisable est satisfaisable et
si l'ensemble des clauses (des deux listes) est
insatisfaisable, et s'il n'y a pas de limite du temps de preuve et de la taille des clauses,
il en déduit la clause vide.
- Preuve en logique du premier ordre
par la méthode dite "Model Elimination"
Etant donné une liste de clauses, le logiciel essaie de construit une preuve de la clause vide
par cette méthode.
Le prouveur est complet : si l'ensemble des clauses est insatisfaisable et s'il n'y a pas
de limite du temps et de la longueur des preuves, il en déduit la clause vide.
Dernière modification : 27-Feb-2023