Discussion :

[millie]

Bonjour,

Un spécialiste de PVS m'a dit que non, mais on ne sait jamais. Est-il possible de restreindre les preuves que l'on fait avec PVS à la logique intuitionniste (donc surtout pour empêcher des preuves utilisant le principe du tiers exclus) ?

Merci

[gorgonite]

ben suffit de savoir sur quel modèle logique il est basé (s'il y en a un )


par exemple, je crois bien que coq sans axiome ajouté peut être considéré comme de la logique intuitionniste... mais on attendra que Steki-kun confirme

[millie]

On m'a dit que PVS reposait sur la logique classique et que si je voulais faire de la logique intuitionniste, il fallait que j'aille voir coq car il utilisait celle là (mais qu'avec coq il était possible d'utiliser la logique classique en chargeant une bibliothèque supplémentaire)

Mais je voulais avoir la confirmation

[Steki-kun]

Je suis pas un expert du PVS, mais le problème ici il me semble, c'est que PVS utilise comme "boites noires" un certain nombre de procédures de décision et pas vraiment le fait qu'il soit basé sur la logique classique au départ. Sinon, en faisant tes preuves, tu pourrais toi-même te restreindre à de la logique constructive, mais là tu n'as pas moyen de savoir si les procédures de décision utilisées pour décharger un certain nombre de buts respectent cette contrainte. Je ne vois cela dit pas de raison particulière pour les procédures de décision que j'ai en tête d'utiliser de la logique classique mais bon, on peut se méfier

Avant de te dire d'utiliser Coq, pour quelle raison as-tu besoin de logique intuitionniste ?

[alex_pi]

Avant de te dire d'utiliser Coq, pour quelle raison as-tu besoin de logique intuitionniste ?

J'avoue que si le but n'est pas d'arriver à un moment à de l'extraction de programme, l'intéret de la logique intuitionniste n'est pas particulièrement flagrant.

[millie]

J'avoue que si le but n'est pas d'arriver à un moment à de l'extraction de programme, l'intéret de la logique intuitionniste n'est pas particulièrement flagrant.

Je n'ai pas de but particulier à l'instant même. Mais des choses qui me trottent dans la tête et il est possible que j'ai besoin de ça pour des raisons autres que l'extraction de programmes (mais c'est pas encore bien clair). Mais de toute façon, peut être que pour ma culture générale, j'essayerai de jeter un œil à coq

Merci à vous tous

[alex_pi]

Mais de toute façon, peut être que pour ma culture générale, j'essayerai de jeter un œil à coq

Si tu veux un bon tuto, je te conseille

http://www.cis.upenn.edu/~plclub/pop...ode/index.html

En tout cas CoqIntro.v est vraiment pas mal. Après, ça se complique un peu trop vite à mon gout.

Have fun ;-)