Les ordinateurs sont-ils logiques ? 2 : Logique des prédicats

lundi 26 octobre 2015
par  Alain BUSSER

Le logiciel CoqIde ressemble à un environnement de programmation mais son moteur est Coq, un logiciel libre qui permet de faire des déductions dans la logique des prédicats. L’article qui suit ressemble à un tutoriel pour Coqide, tout simplement parce qu’un tel tutoriel n’existe pas !


Le coq et l’outre

Coq permet, on le verra ci-dessous, de guider l’utilisateur dans la construction de la preuve ; Par exemple, si on pense des choses comme "et si j’utilisais l’axiome A1, est-ce que je peux y arriver ?", Coq permet de faire rapidement le test et de voir ce qu’il reste alors à faire.

Mais Coq ne permet pas d’avoir automatiquement la preuve, celle-ci reste de la responsabilité de son utilisateur. Otter est une sorte de logiciel de calcul formel dans une algèbre de Boole et peut, lui, fournir automatiquement la preuve d’un théorème qu’on lui soumet. Intéressant, si au bout d’un certain temps, la preuve ne vient pas, on peut essayer son côté sombre Mace qui, lui, cherche un contre-exemple. Otter n’est plus développé, mais il lui succède Prover9 qu’on peut installer ou tester en ligne.

Ci-dessous on va montrer comment Coq aide à démontrer des syllogismes et à chaque fois, on va comparer avec la version Otter prover9. Toutefois, Prolog quand à lui, est capable de trouver tout seul une démonstration.


Documents joints

HTML - 1.8 kio
HTML - 2.3 kio

Commentaires