Home

pdf, 708 K - Université Laval

1. commande i instantiate instanciations instanciations let d f let d f let d f nom variable expression Cette commande est utile pour instancier une ou plusieurs variables quan tifi es Toutes les variables que l on souhaite instancier doivent apparaitre dans le m me pr dicat quantifi Par exemple on ne pourrait pas instancier p et q en m me temps dans ce but Vp Z p 1leVq Ze mais on pourrait r aliser cela si le pr dicat tait plut t Vp q Z e Bien entendu l expression donn e dans la commande est v rifi e par rap port au type pour que l expression respecte le but courant Cette commande est utile lorsqu on souhaite v rifier une galit possible entre des variables diff rentes dans deux quantifications diff rentes Prenex La commande prenex poss de la syntaxe suivante commande prenex Le fonctionnement de cette commande est simple Tout d abord le d mon strateur tente de transformer tous les quantificateurs en quantificateurs uni versels Ensuite Z EVES enl ve les quantificateurs universels qui sont domi nants les premiers que l on traite et transforme le but courant en ajoutant aux hypoth ses pour le pr dicat trait que chaque variable li e devient une variable l ment du type de l ensemble sp cifi par la quantification Par exemple si le but courant est Vp BoolGries e p V p vrai alors la commande prenex donne le but quivalent suivant p
2. theorem Affaiblissement5 Vp q r BoolGries e p q p qV r vrai proof apply DistEtSurOu1 simplify use lemme22 p p q q p q T p r apply ReflexiviteDeImplication simplify apply ZeroDeOu2 to expression vrai V p q p r simplify with disabled implicationDef ouCommutativite ouAssociativite DeMorgan1 DeMorgan2 etCommutativite etAssociativite DistOuSurEt1 DistEtSurOul RegleDOr prove theorem ModusPonens Vp q BoolGries e p p gt q gt q vrai proof use DefAltDeImplication1 use DefAltDeImplicationl p p p V q use DeMorgan2 p p p V q use DeMorganl q p V q use DeMorgan2 p p 152 theorem ModusPonens suite de la preuve pr c dante Vp q BoolGries e p p gt q gt q vrai proof apply DoubleNegation to expression p simplify with disabled RegleDOr implicationDef DistOuSurEt1 DistEtSurOu1 DeMorgan1 DeMorgan2 ouCommutativite ouAssociativite etAssociativite etCommutativite prove apply RegleDOr to expression p q simplify with disabled RegleDOr implicationDef DistOuSurEt1 DistEtSurOul DeMorgan1 DeMorgan2 ouCommutativite ouAssociativite etAssociativite etCommutativite DistNegSurEquiv1 DistOuSurEquiv1 prove apply ouCommutativite to expression p V p simplify apply TiersExclu to expression p V p simplify apply ouCommutativite to expression p V q simplify use lemmel6 p q q p with disabled RegleDOr
3. BoolGries non peutEtre peutEtre end theorem alors ceci aurait cr er un effet trange a notre logique Cet axiome aurait rendu notre logique univalu e Donc nous n aurions pas tendu mais plut t restreint notre alg bre Il est facile de s en convaincre Tout d abord pensons que p dans l axiome du tiers exclu prend la valeur peut tre D s cet instant nous obtenons le cas particulier suivant peut tre V peut tre vrai En utilisant l axiome peut EtreN egation on obtient le r sultat suivant peut tre V peut tre vrai Ce qui se r duit avec l idempotence de la disjonction en peut tre vrai Ensuite imaginons que p dans le th or me de la contradiction prend la valeur peut tre ce moment l nous obtenons le cas particulier suivant peut tre peut tre faux En utilisant l axiome peut EtreN egation on obtient ceci peut tre peut tre faux Ce qui se r duit avec l idempotence de la conjonction en peut tre faux Donc on obtient vrai faux peut tre Ce qui permet de dire que notre logique est univalu e elle est contradictoire Ce qui n tait pas le r sultat voulu au d part car nous voulions tendre notre logique Nous n avons r ussi qu la restreindre par l ajout de cette nouvelle constante 70 C est pour cela qu il faut faire tr s attention lorsque nous tentons d tendre cette alg bre l aide de nouvelles constantes Une dern
4. Donnons lui la commande prove et voyons comment il se d brouille prove Nous nous rendons compte que Z EVES n a pas vraiment progress Il reste en fait au but p Mn BoolGries NN land q Nin BoolGries NN land r Min BoolGries NN implies p Nou q Nou r p Nou q Nou p Vou r vrai dire le d monstrateur n a utilis que l associativit de la disjonc tion avec cette commande Donc ce n est pas un bon d but Recommencons 62 donc en d cidant de le diriger Tapons tout d abord retry pour revenir au d but de la d monstration au but initial Ensuite servons nous de la preuve r alis e plus haut pour nous aider dans notre direction de Z EVES premi re vue nous voyons que la d monstration est un peu complexe et qu elle n cessite beaucoup d tapes Ce qui pourrait nous aider ce moment l est un lemme Pour tenter de d montrer le th or me nous allons utiliser l heuristique de la progression par les deux bouts voir 4 pour la description de cette heuristique Tout d abord ten tons de voir ce qui serait simple d montrer dans notre preuve Nous pour rions s parer notre preuve en deux parties la premi re partie consisterait d montrer que Vp q r BoolGries e p V q V r z p V p V q V r et la deuxi me partie consisterait en la d monstration de Vp q r BoolGries p V p V qVr p V q V p V r Ces deux parties repr senteront donc deux lemmes que nous pourrons
5. Z EVES peut faire grace nos r gles de r criture sans que nous l aidions rewrite Nous nous rendons compte que nous n avons pas beaucoup progress car Z EVES a d cid d utiliser l axiome de l idempotence de la disjonction pour r duire le th or me Il faut donc d sactiver ce th or me pour permettre de progresser quelque peu Commengons par revenir au but initial par la com mande retry et donnons lui une commande plus sp cifique with disabled ouIdempotence rewrite Voil le but courant que Z EVES nous retourne p Mn BoolGries NN land q in BoolGries NN land r Min BoolGries NN implies p Vou p Nou q Vou r p Vou q Vou p Vou r Nous avons progress quelque peu Il s agit maintenant de commuter p et q dans cette expression et le tour est jou Commencons par permuter tout d abord q et p V r dans l expression q V p V r Ce qui se traduit en Z EVES par la commande apply ouCommutativite to expression q Vou p Vou r Z EVES donne la nouvelle expression sous une forme conditionnelle mais elle est tout de m me compr hensible Maintenant v rifions si le d monstrateur est capable de terminer la preuve seul en lui donnant la commande rewrite 64 Finalement Z EVES nous apprend qu il a t capable de terminer la preuve seul en nous retournant le but courant true Nous avons donc notre lemme7 qui est op rationnel Nous avons maintenant tous nos outils pour notre d monstration du th or me
6. la diff rence que l usage d un th or me peut varier si un th or me est utile pour rendre plus automatique les d monstrations alors on lui d cerne l usage rule r gle de r criture sinon on ne lui donne aucun usage Pour savoir si un th or me est utile pour rendre le d monstrateur automatique de th or mes plus performant on s est fi son nombre d oc currences dans les preuves des th or mes Les th or mes dont le nombre d occurrences tait lev ont obtenu un statut de r gle de r criture Autre diff rence entre les th or mes et les axiomes les preuves Pour chaque th or me nous avons trouv une preuve possible pas n cessairement la meilleure dans Z EVES Pour trouver les preuves nous r alisions les d monstrations dans le mode graphique et transcrivions ensuite cette preuve dans un fichier Z BATEXS Une telle technique tait utilis e parce que les 18Pour l instant il n existe aucun outil dans ce logiciel qui permet de passer du mode graphique au mode textuel 46 d monstrations sont beaucoup plus naturelles et visuellement plus faciles comprendre dans le mode graphique Le d savantage est que l on ne sait pas quels th or mes Z EVES avait utilis s pour se rendre au but courant Donc on le transformait dans le mode textuel pour pouvoir connaitre les th or mes utilis s Les th or mes sont entr s de la m me mani re que d finie dans la section 5 2 5 Voil un exemple
7. mais la syntaxe est diff rente La description des commandes s inspire grandement de celle r alis e dans 16 10Ces commandes seront marqu es de ce signe x x x 30 Z EVES fonctionne selon la m thode du but fix Cette m thode utilise le th or me qu on demande de r soudre par le d monstrateur et celui ci devient le but principal En entrant des commandes on dirige Z EVES pour qu il puisse l aide de ses axiomes de base et de ses regles de r criture tenter de r duire le plus possible ce but un but quivalent qui est appel le but courant Une d monstration est consid r e termin e lorsque le but courant est le pr dicat true Donc si le but courant n est pas true on essaie de le r duire pour l obtenir 5 2 6 1 Commandes pour s parer un but en sous buts Quelquefois les preuves sont ardues et on a de la difficult cerner le probl me dans son entier ce moment l des commandes peuvent servir pour s parer un but courant en plusieurs sous buts dont leur ensemble est quivalent Ces commandes sont Cases La commande cases poss de cette syntaxe commande cases Cette commande s pare le but en plusieurs sous buts si le but est e une conjonction e une disjonction e un pr dicat conditionnel e une implication dont le cons quent a une des formes mentionn es plus haut Le but est donc s par en sous buts et Z EVES donne visuellement un des sous buts pour qu on puisse continuer de le
8. or me est d montr Deuxi me preuve du th or me Cette preuve est plus longue que la premi re mais elle permet de r aliser toutes les tapes de la d monstration manuellement Avant de d buter Jl faut conna tre une subtilit de la fen tre Proof de Z EVES pour pargner du temps dans les d monstrations La petite fen tre Formula la partie basse de la fen tre Proof permet de s lectionner une par tie d un th or me seulement et si nous cliquons sur le bouton de droite de la souris nous pouvons appliquer des commandes d j programm es dans Z EVES ces commandes sont sp cifiques chaque expression ou pr dicat s lectionn En tant que tel ceci n est qu un raccourci pour r aliser les preuves nous pouvons r aliser n importe quelle preuve sans jamais nous en soucier mais quelque fois il est pr f rable de miser sur la rapidit de la d monstration Cette subtilit renferme beaucoup de commandes utiles pour les d monstrations D monstration Il faut appliquer dans l ordre les commandes suivantes pour r ussir d montrer le th or me 1 apply DistOuSurEquiv2 to expression p ou q ou p equiv p 2 simplify 3 apply ouldempotence to expression p ou p 4 simplify 74 apply ouCommutativite to expression p ou q ou p simplify apply ouAssociativite to expression q ou p ou p simplify apply ouldempotence to expression p ou p Se KR 5 m 10 simplify 11 apply ouCommutativite to expression
9. q p V p q En utilisant la commande apply nom th or me seulement alors Z EVES tentera d appliquer la r gle de r criture partout o cela est possible dans le but Si une expression ou un pr dicat particulier est sp cifi une expression est sp cifi e par to expression et un pr dicat par to predicate alors le d monstrateur appliquera la r gle si possible seulement aux occurrences de l expression ou du pr dicat d sir Invoke Cette commande a la syntaxe suivante commande invoke nom v nement invoke predicate pr dicat nom sch ma nom d finition nom v nement La commande invoke permet de remplacer dans le but courant toutes les occurrences du nom d un sch ma ou du nom d une d finition sp cifi e par leur d finition respective Si aucun nom n a t sp cifi dans la commande alors tous les noms de sch mas ou de d finitions seront remplac s par leur d finition La commande invoke predicate est semblable la commande invoke sauf que l on sp cifie un nom de pr dicat dans la commande invoke predi cate La grande diff rence se situe dans la fa on dont Z EVES interpr te les commandes Par exemple si on dirige le d monstrateur en donnant la com mande invoke S o S est un sch ma et qu au m me moment le but courant contient des r f rences S et S S est le sch ma S d cor on a comme r sultat que chacune des occurrences de S sont remplac es par la d finition de
10. retry La commande retry enl ve et perd toutes les tapes de la preuve r alis es jusqu pr sent et met le but courant de la d monstration dans sa forme initiale 5 2 6 7 Autre commande utile Il existe une autre commande qui est r s utile pour la d monstration de th oremes dans Z EVES et qui est d finie tr s sommairement dans 16 prove Cette commande poss de la syntaxe suivante commande prove A vrai dire la commande prove a d ja t d finie dans la section 5 2 6 2 2 La commande prove est le diminutif de la commande prove by rewrite Donc dans l interface graphique de Z EVES vous ne trouverez que la commande prove dans les options du bouton reduction Gardez toujours l esprit que cette commande est la m me que prove by rewrite 5 2 7 Formalisme des donn es d entr e Maintenant que vous connaissez les diff rentes fen tres de Z EVES dans les deux modes ainsi que la syntaxe de base de Z EVES et que vous avez pris connaissance de la syntaxe que la pr sente recherche a implant e dans Z EVES vous tes pr t comprendre comment nous avons r ussi donner ce d monstrateur cette panoplie d axiomes et de th or mes Mode textuel Comment entrer un axiome Tout d abord Z EVES hait ne pas connaitre le type d une variable utilis e dans un th or me Il faut donc toujours d clarer le type de chaque variable 43 soit l aide d un type pr d fini soit l aide d un type que vous lui
11. 1 5 2 A 1 A 2 A 3 A 4 A 5 A 6 A T A 8 Tableau de la syntaxe de la logique propositionnelle Interface Z ATEX de Z EVES sous la plateforme Windows Grammaire utilis e pour la formation des pr dicats Tableau sur les diff rences entre les d monstrateurs automa tiques de th or mes suivant les crit res de comparaison pla teforme langage de base et puissance maximale Tableau sur les diff rences entre les d monstrateurs automa tiques de th or mes suivant les crit res de comparaison pla teforme langage de base et puissance maximale suite Tableau sur les diff rences entre les d monstrateurs automa tiques de th or mes suivant les crit res de comparaison pla teforme langage de base et puissance maximale suite Tableau sur les diff rences entre les d monstrateurs automa tiques de th or mes suivant les crit res de comparaison pla teforme langage de base et puissance maximale suite Tableau sur les diff rences entre les d monstrateurs automa tiques de th or mes suivant les crit res de comparaison pla teforme langage de base et puissance maximale suite Tableau sur les diff rences entre les d monstrateurs automa tiques de th or mes suivant les criteres de comparaison qua lit de la bibliographie et type d interaction Tableau sur les diff rences entre les d monstrateurs automa ti
12. 5 p V p vrai proof use ouCommutativite p p q p rewrite theorem rule ZeroDeOul Vp BoolGries e p V vrai vrai proof use equivIdentite2 rewrite theorem rule ZeroDeOu2 Vp BoolGries e vrai V p vrai proof rewrite Ajout de lemmes theorem lemme3 Vp BoolGries e p V faux p V ap p proof use TroisPointDixHuit2 rewrite theorem lemme4 Vp BoolGriese pV p p p vrai proof use DistOuSurEquiv2 q p r p rewrite use equivIdentite5 prove theorem lemme5 Vp BoolGries e p V faux p vrai proof use lemme3 use lemme4 rewrite 125 Fin de l ajout de lemmes theorem rule ouldentitel Vp BoolGries e p V faux p proof use lemmed rewrite theorem ouldentite2 V p BoolGries e faux V p p proof apply ouCommutativite to expression faux V p with disabled equivldentite2 fauxDef rewrite Ajout de lemmes theorem lemme6 Vp q r BoolGries ep V qV r pV pV qv r proof prove theorem lemme7 Vp q r BoolGriesep V pV qV r pV qV pV rm proof with disabled ouldempotence rewrite apply ouCommutativite to expression q V p V r rewrite Fin de l ajout de lemmes theorem DistOuSurOul Vp q r BoolGries ep V qV r pV qV pV r proof use lemme6 use lemme7 rewrite 126 theorem DistOuSurOu2 Vp q r BoolGries ep V qV pV r 2 pV qv r proof use DistOuSurOul prove theorem TroisPointQuaranteDeux1 Vp q BoolGriesep V q pV q p proof rewrit
13. 6 Une derni re chose est importante lorsque vous utilisez l interface tex tuelle C est l utilisation de la touche Break sur le clavier Elle est importante car elle permet de gagner du temps lorsque vous savez que Z EVES travaille sur une preuve et qu il semble tre perdu dans un trop grand nombre de possibilit s Appuyez sur cette touche celle ci vous permettra d arr ter la tentative en cours Entrez des commandes plus pr cises et ensuite relancez Z EVES Ceci vous fera conomiser du temps Mode graphique L utilisation de l interface en mode graphique est naturelle Cette inter face est conviviale Pour bien comprendre les diff rentes fen tres et leurs commandes respectives lisez la section 2 2 du manuel 18 La commande pertinente pour cette recherche est une de celles qui se re trouvent dans la fen tre Specification dans le menu File la commande Im port Cette commande puissante permet d importer des fichiers Z IATEX dans l interface graphique Dans cette recherche elle est utile pour charger la banque de th or mes et d axiomes de la logique de Gries amp Schneider pour pouvoir travailler avec Le seul d faut de cette commande pour l instant est de ne pas importer les preuves dans l interface graphique Donc on a la banque de th or mes mais on n a pas les d monstrations de ces th or mes il faut les refaire soi m me 23 5 2 5 Syntaxe du d monstrateur Z EVES fonctionne sous deux formes de syntaxe cel
14. Les crit res de comparaison Quatre vingt d monstrateurs automatiques de th or mes ont t tudi s dans cette recherche Pour chacun de ces d monstrateurs on a v rifi des criteres permettant d orienter une d cision pour obtenir le d monstrateur automatique de th or mes le plus adapt aux besoins que nous avions Ces d monstrateurs ont t compar s suivant ces crit res e Les plateformes sur lesquelles le d monstrateur automatique de th o remes fonctionne Nous recherchons un d monstrateur fonctionnant sur la plateforme adopt e par la majorit des tudiants en informatique l universit Laval Windows e La qualit de la bibliographie offerte pour supporter l apprentissage et la connaissance du logiciel Nous recherchons simplement une biblio graphie ayant une bonne quantit d information pertinente pour mieux comprendre et apprivoiser le d monstrateur automatique de th or mes e Le co t de l implantation du d monstrateur automatique de th or mes De pr f rence nous utiliserons un d monstrateur ayant un faible co t ILes crit res sont class s en ordre d croissant de priorit d implantation pour des tudiants e La puissance maximale que le d monstrateur peut atteindre les diff rentes logiques qu il supporte Nous nous limitons la logique classique de premier ordre dans le cadre de cette recherche e Le langage de programmation sur lequel est construit le d monstrateur aut
15. Vp q r BoolGries e p V q r S pq p r DefAltDelmplication1 3 72 Vp q r BoolGries e p V q Ar S p V q p r DefAltDeImplicationl 3 72 avec q r Vp q r BoolGries e p V q r 2p V q p V r DistOuSurEt1 avec p p Donc nous avons d montr le th or me Troisi me exemple ExTheoLongLogProp tex Le troisi me th or me qui sera d montr est un th or me tir de la banque de th or mes que nous avons r alis dans cette recherche C est le th or me Vp q BoolGriesep Vq p qzspzq Il a t choisi car c est un th or me qui poss de une preuve plut t com plexe dans Z EVES et ce th or me a une signification int ressante En effet ce th or me donne un lien possible pour cr er une quivalence gr ce aux op rateurs gt Vet A Ce th or me et sa d monstration sont pr sent s dans le fichier ExTheo LongLogProp tex Nous donnons dans l ordre les commandes appliquer dans le mode graphique pour permettre de d montrer ce th or me 1 M gt S 9o 23 m Ay DSO apply implicationDef to expression p ou q implique p et q simplify use DistOuSurEtl p p ou q q p r q apply ouAssociativite to expression p ou q ou p simplify apply ouCommutativite to expression q ou p simplify use lemmel14 apply ouAssociativite to expression p ou q ou q simplify 76 11 apply ouldempotence to expression q ou q 12
16. d monstration complexe et simple convivialit et niveau d int r t 102 Convivialit niveau complexe d int r t A ACL2 Lente et difficile CLIN CLIN S Z z Z gt gt S Z Fic A 16 Tableau sur les diff rences entre les d monstrateurs automa tiques de th or mes suivant les crit res de comparaison rapidit avec d monstration complexe et simple convivialit et niveau d int r t 103 Convivialit niveau d int r t FINDER A A N A h Frapps FT HR Fic A 17 Tableau sur les diff rences entre les d monstrateurs automa tiques de th or mes suivant les crit res de comparaison rapidit avec d monstration complexe et simple convivialit et niveau d int r t suite 104 Convivialit Nathm the Boyer Moore prover OSHL Fic A 18 Tableau sur les diff rences entre les d monstrateurs automa tiques de th or mes suivant les crit res de comparaison rapidit avec d monstration complexe et simple convivialit et niveau d int r t suite 105 Convivialit niveau d int r t Fic A 19 Tableau sur les diff rences entre les d monstrateurs automa tiques de th or mes suivant les crit res de comparaison rapidit avec d monstration complexe et simple convivialit et niveau d int r t suite 106 d Otter et de FINDER Fic A 20 Tableau sur les diff rences entre les d monstrateurs automa tiques de th or m
17. d montre de la m me mani re que dans le mode textuel Ce qui veut dire que vous n avez qu appliquer la commande rewrite qui se situe dans le menu du bouton Reduction V rifiez si dans la fen tre du bas le pr dicat est true Ceci signifie que la d monstration de ce lemme est termin e Revenez la fen tre principale donnant acc s tous vos th or mes et axiomes Pour cela cliquez sur le bouton Window et s lectionnez l option Specification Il faut maintenant r aliser la preuve du lemme lemme7 Acc dez la fen tre Proof de la m me mani re que vous avez utilis e pour acc der celle du lemme lemme6 Il faut prouver ce th or me Vous pouvez le prouver exactement comme dans le mode textuel Pour cela il vous faut entrer les commandes manuellement Tout d abord s lectionnez la commande New Command dans le menu Edit Dans la fen tre blanche de l diteur crivez l instruction 26Le mode graphique n utilise pas le comme fin d instruction phiq P 66 with disabled ouldempotence rewrite Ensuite s lectionnez la commande Done dans le menu File Ceci vous ram ne la fen tre Proof avec si tout s est bien d roul le texte de la commande que vous avez entr au clavier Cette commande devrait tre affect e d un point d interrogation sa gauche pour sp cifier qu elle n a pas encore t activ e Activez la en cliquant avec le bouton droit de la souris sur le texte de la commande et
18. d entrer dans le mode Z lATEX Cette interface est simple d utilisation La syntaxe pour entrer des sp cifi cations en Z est donn e la section 5 2 5 Cette section se propose de donner un apercu des options possibles de cette interface Une fois que vous avez d but le d monstrateur automatique de th o r mes dans le mode textuel comme pr sent la section 5 2 3 vous vous retrouvez devant une fen tre comme celle pr sent e la figure 5 1 Cette interface est simple Il y a peu de commandes accessibles par le menu Il faut entrer au clavier le reste des sp cifications que vous d sirez 3Cette section du mode textuel est bas e en grande partie sur le document 15 21 1 CL for Windows ight C 1992 1997 Franz Inc Berkeley CA USA JE ge gt Fic 5 1 Interface Z lATEX de Z EVES sous la plateforme Windows 22 La barre de menu se compose de quatre diff rents menus File Edit Window et Browser Ces quatre menus permettent l acc s des commandes de base Pour bien comprendre et assimiler ces commandes de base lisez la section 5 1 du manuel d instruction 15 La commande importante dans le menu est celle pour lire des fichiers en mode batch Elle est importante et int ressante car elle permet de lire un fichier d j crit en Z lATEX pour visualiser ses r sultats Donc on peut s en servir pour faire tourner des exemples d j programm s Cette commande sera utile pour le chapitre
19. de la m me mani re qu ils sont repr sent s dans le mode graphique de Z EVES 29 les op rateurs ajout s dans Z EVES par cette recherche il suffit d utiliser la syntaxe d finie ci dessous Syntaxe de Symbole de Exemple Priorit l op rateur l op rateur d utilisation equiv p equiv q 3 nonequiv ES p nonequiv q 3 implique gt p implique q 4 consequence lt p consequence q 4 et petq 5 ou V p ou q 5 non A non p 9 Les caract res sp ciaux les symboles sont accessibles dans le mode gra phique grace aux boutons de commandes et leur macro respective mais les commandes IATEX entr es au clavier comme si vous tiez dans le mode tex tuel ne fonctionnent pas Il faut absolument utiliser leur homologue gra phique Les m mes axiomes et th or mes que ceux d finis dans le mode textuel fonctionnent et peuvent tre utilis s dans le mode graphique 5 2 6 Commandes du d monstrateur Les commandes permettant de diriger le d monstrateur fonctionnent tout aussi bien dans le mode textuel que graphique sauf qu il y a des commandes qui ne fonctionnent que dans le mode textuel Pour entrer des commandes de facon manuelle dans le mode graphique il faut s lectionner dans le menu de la fen tre Proof Edit New Command Ceci vous am nera dans le mini editor qui vous permettra d entrer vos com mandes Ces op rateurs sont les m mes que dans le mode textuel
20. disabled permet de d sactiver temporairement le temps d une commande des th or mes des d finitions ou des d clarations Ceci permet d ex cuter une commande de r duction automatique pr sent e la section 5 2 6 2 2 en enlevant des v nements dont on ne souhaite pas se servir Tenter de d sactiver un v nement d j d sactiv n a aucun effet 40 Cette commande a t extr mement utile lors de la pr sente recherche car Z EVES fonctionne d une fa on s quentielle pour l utilisation de ses r gles de r criture Lorsqu on d sirait se servir d un th oreme qui r sidait vers la fin de la liste de th or mes ou que l on d sirait enlever une d finition qui risquait d tre g nante pour le restant de la d monstration alors on d sactivait les th or mes qu on ne voulait pas utiliser Ceci permet de gagner un temps consid rable dans les preuves car le nombre de cas possibles diminue lorsqu on restreint le nombre de th or mes dont on peut se servir Par exemple on souhaite prouver le th or me suivant Vp q r BoolGries e p q r p q p r On peut le d montrer rapidement gr ce aux th or mes de la conjonction seulement Donc si on d sire utiliser ces th or mes d une fa on automatique sans utiliser la regle d or qui sera appliqu e en premier car elle est positionn e plus avant dans la liste de th or mes que les th or mes de la conjonction il faut d sactiver la r gle d or pour rendre cel
21. es pour l analyse des diff rents d monstrateurs automatiques de th or mes A 22 Adresses Internet utilis es pour l analyse des diff rents d monstrateurs automatiques de th or mes suite A 23 Adresses Internet utilis es pour l analyse des diff rents d monstrateurs automatiques de th or mes suite A 24 Adresses Internet utilis es pour l analyse des diff rents d monstrateurs automatiques de th or mes suite A 25 Adresses Internet utilis es pour l analyse des diff rents d monstrateurs automatiques de th or mes suite vi R sum Les logiciels se d veloppent de plus en plus rapidement Pour pouvoir suivre le courant il faut que les compagnies produisent leurs logiciels en un temps toujours plus restreint On peut r duire le temps de production en d montrant que les sp cifications du logiciel sont tanches Ces d monstrations sont sou vent fastidieuses En utilisant un d monstrateur automatique de th oremes les preuves deviennent plus ais es et cela permet donc de r duire le temps de v rification des sp cifications Ce document vise montrer les diff rents d monstrateurs automatiques de th or mes existants pr sentement Aussi il est pr sent ici un manuel d utilisation pour le d monstrateur automatique de th or mes Z EVES ver sion 2 1 Ce document pr sente la logique quationnelle de Gries amp Schneider 5 comme pilier pou
22. et huit secondes Si vous d sirez travailler avec seulement une partie de la banque de th or mes vous devez connaitre les th or mes et les axiomes que vous sou haitez utiliser Ensuite pour chacun de ces axiomes et th or mes il faut s ils ne sont pas dans un ordre s quentiel cliquer sur le bouton droit de la souris sur chacun d eux et il faut s lectionner la commande Check dans le menu d roulant Il faut pr alablement que vous ayez op r cette commande Check sur le type BoolGries ainsi que sur chacun des op rateurs et des constantes de ce type Si vous voulez charger seulement une partie de la banque de donn es mais que celle ci se pr sente d une fa on s quentielle alors vous pouvez simplement suivre les intructions donn es pour le chargement des th oremes dans le mode graphique pour toute la banque de th or mes mais vous ex cutez la derni re commande sur le dernier th or me que vous sou haitez traiter 97 C tait les m thodes rapides pour charger la banque de donn es utilis e lors de cette pr sente recherche Comment modifier cette banque On peut modifier la banque d axiomes et de th or mes soit en ajoutant un axiome ou un th or me soit en enlevant un th or me si on enl ve un axiome alors ceci change totalement le syst me d axiomes et on risque de ne plus pouvoir prouver certains th or mes Pour ajouter un axiome ou un th or me Il y a deux mani res d ajouter un axiome ou un th
23. expression p q simplify prove by reduce theorem rule DoubleNegation Vp BoolGries e 3 2p p proof use DistNegSurEgalite p p q p prove 122 theorem DoubleNegation2 Vp BoolGries e p p proof prove theorem fauxNegation V p BoolGries e faux vrai proof prove theorem TroisPointDixSept Vp q BoolGriesep q 7p q proof prove by reduce theorem TroisPointDixHuit1 Vp BoolGries e p p faux proof use DistNegSurEquivl q p rewrite theorem TroisPointDixHuit2 Vp BoolGries e faux p p proof use TroisPointDixHuitl rewrite theorem rule nonequivCommutativite Vp q BoolGriese p q qF p proof rewrite 123 theorem rule nonequivAssociativite Vp q r BoolGries e p qx r pz qr proof use nonequivDef use DistNegSurEquiv1 rewrite apply equivCommutativitel to expression r p q simplify rewrite apply equivCommutativitel to expression q r simplify apply DistNegSurEquiv2 to expression r q simplify apply equivCommutativitel to expression r q simplify rewrite theorem AssociativiteMutuelle Vp q r BoolGriesep q r p q r proof rewrite theorem InterchangeabiliteMutuelle Vp q r BoolGriesep q r p qF r proof rewrite Th or mes de la disjonction theorem ouAssociativite2 Vp q r BoolGriesepV qV r 2 pVqvr proof prove theorem ouldempotence2 Vp BoolGries e p p V p proof rewrite 124 theorem TiersExclu2 Vp BoolGries e
24. expression q V q simplify apply etldempotence to expression p V q p V q simplify apply RegleDOr to expression p q simplify apply equivCommutativitel to expressionp V q p q p V q simplify use equivAssociativitel p p q q p V q r p V q apply equivIdentitelto expression p V q p V q simplify with disabled ouAssociativite ouCommutativite prove theorem rule ReflexiviteDelmplication V p BoolGries e p p vrai proof prove theorem ZeroADroiteDeImplication V p BoolGries e p vrai vrai proof prove 148 theorem IdentiteAGaucheDeImplication Vp BoolGries e vrai gt p p proof prove theorem TroisPointQuatreVingtSept Vp BoolGries e p gt faux 7 p proof prove theorem TroisPointQuatreVingtHuit Vp BoolGries e faux gt p vrai proof prove use ouldentite1 use faux Def prove theorem Affaiblissement1 Vp q BoolGries e p gt p V q vrai proof prove use lemmel4 prove 149 theorem Affaiblissement2 Vp q BoolGries e p q gt p vrai proof use DefAltDeImplication2 p p q q p apply etAssociativite to expression p q p simplify apply etCommutativite to expression p q p simplify apply etAssociativite to expression q p p simplify apply etIdempotence simplify apply etCommutativite to expression q p simplify apply equivIdentitelto expression p q p q simplify with disabled RegleDOr implicationDef prove theorem Affaiblissement3
25. l alg bre bool enne 114 D finition du type BoolGries BoolGries D finition des op rateurs pour la syntaxe syntax infun3 syntax infun3 syntax V infund syntax infund syntax gt infun4 syntax lt 4 infun4 syntax lt inrel D finitions des constantes et du typage des op rateurs vrai BoolGries faux BoolGries _ _ BoolGries x BoolGries BoolGries BoolGries x BoolGries BoolGries V _ BoolGries x BoolGries BoolGries _ BoolGries x BoolGries BoolGries _ _ BoolGries x BoolGries BoolGries _ lt _ BoolGries x BoolGries BoolGries BoolGries BoolGries _ lt _ BoolGries BoolGries enabled rule pluspetitqueDef Vp q BoolGries e p lt q amp p q vrai Axiomes de base Axiomes de l quivalence theorem rule equivAssociativitel Vp q r BoolGriesepzqzsr pz qzr 115 theorem rule equivAssociativite2 Vp q r BoolGriese p q r p q r theorem rule equivCommutativitel Vp q BoolGriesep q q p theorem equivCommutativite2 Vp q BoolGriesep q q D theorem rule equivCommutativite3 Vp q BoolGriesep q q p theorem rule equivIdentitel V p BoolGries e p p vrai theorem rule equivIdentite2 Vp BoolGries e vrai p p theorem rule equivIdentite3 Vp BoolGries e vrai p p theorem equivIdentite4 V p BoolGries e p vrai p Axiome de faux theorem rule fauxDef Vp BoolGries e faux 7 vrai Axiomes de la n gat
26. le d monstrateur nous indique qu il a utilis ces r gles de transfert avec les hypoth ses donn es autant les hypoth ses du but courant que celles des diff rents th or mes utilis s pour la d monstration Finale ment la commande se termine en nous donnant le but courant prouver p Mn BoolGries NN land q Nin BoolGries NN implies non p equiv q equiv non p q Ensuite Z EVES passe l autre commande invoqu e de facon s quentiel le et applique la r gle de r criture equivCommutativitel seulement aux occurrences de l expression Anon p equiv q Cette r gle de r criture a t appliqu e de la facon que Z EVES se repr sente les op rateurs l interne Donc le bout de th or me modifi par cette com mande est mis sous la forme conditionnelle Cette commande correspond la section de la preuve suivante dans le r sultat Applying equivCommutativitel to Anon p equiv q gives 22Une commande se termine toujours en nous donnant le but courant prouver 52 p Mn BoolGries NN land q Nin BoolGries NN implies IF non p in BoolGries land q in BoolGries THEN q equiv non p ELSE non p equiv q equiv non p q Pour continuer Z EVES ex cute la troisi me commande la commande simplify Cette commande se lit de la m me mani re que la commande reduce dont l explication a t donn e plus haut Voila la section qui corres pond cette commande Which simplifies forward cha
27. mes de cette alg bre bool enne Z EVES et voir sa r action Nous avons r alis ceci et nous nous sommes rendus compte que Z EVES se pr tait tr s bien la d monstration des th or mes de la logique quationnelle de Gries amp Schnei der Les preuves sont naturelles et int ressantes Parfois Z EVES utilisait m me des chemins auxquels nous ne pensions pas prime abord Sauf qu il faut savoir bien diriger ce d monstrateur pour obtenir de bons r sultats ra pidement Les th or mes d montr s par Z EVES sont donn s dans l annexe C ainsi que leur d monstration Avant de vous y r f rer nous vous invitons d abord vous familiariser avec la syntaxe de Z EVES en mode graphique donn e la section 5 2 5 et les diff rentes commandes utilis es dans les d monstrations voir section 5 2 6 Mode graphique Le mode graphique est beaucoup plus simple d utilisation que le mode textuel En mode graphique pour entrer un texte si la fen tre specification est affich e il faut choisir dans le menu Edit New paragraph Ensuite la fen tre du Mini editor apparait ce moment l vous pouvez entrer votre sp cification Z dans notre cas soit un th or me ou un axiome dans la fen tre de texte Pour r aliser les caract res sp ciaux du Z il y a d j des boutons de commandes pr vus cet effet ainsi que leur macro respective Pour utiliser Les th or mes et les axiomes des annexes B et C sont donn s
28. ouAssociativite2 g p r q rewrite Ajout de lemme theorem lemme13 Vp q BoolGrieseq pV q qV p proof apply ouCommutativite to expression p V q simplify apply equivCommutativitel to expression q q V p simplify use TroisPointQuaranteDeux3 p q q p rewrite Fin de l ajout de lemme theorem Absorption3 Vp q BoolGriesep pV qg p q proof rewrite use DistOuSurOul r p rewrite use lemme13 prove 133 theorem Absorption4 Vp q BoolGriesep V p q pVq proof rewrite use DistOuSurOul r p rewrite Ajout de lemme theorem lemme14 Vp q BoolGriese pV pV qg pV q proof use ouAssociativite2 q p r q rewrite Fin de l ajout de lemme theorem rule DistOuSurEt1 Vp q r BoolGries e p V q r p V q pV r proof rewrite apply ouCommutativite to expression q V p V r simplify use lemmel4 q rvV q with disabled ouCommutativite rewrite prove theorem DistOuSurEt2 Vp q r BoolGries e pV q pV r 2 pV q r proof with disabled RegleDOr prove 134 theorem rule DistEtSurOul Vp q r BoolGries e p qV r p q V p r proof rewrite apply DistOuSurEquiv2 to expression p V r p V q simplify apply equivCommutativitel to expression q V r p pV q simplify apply ouCommutativite to expression r V p V q simplify apply ouAssociativite to expression p V qV r simplify rewrite apply equivCommutativitel to expression q V r p pV r sim
29. pr dicats qu on peut r f rencer gr ce leur tiquette De plus on peut donner l tat d un pr dicat dire si ce pr dicat est actif ou non durant la v rification de la sp cification 24 La grammaire suivante est celle utilis e dans cette pr sente recherche sp cification objet de sp c objet de sp c objet de sp c d cl_syntaxe paragraphe Z d cl_syntaxe syndef phrase_ou_mot classe_op phrase_ou_mot phrase_ou_mot phrase mot classe_op infuni infun2 infun3 infun4 infund infun6 ingen pregen inrel prerel postfun word ignore paragraphe Z bo te zed th or me boite zed begin para_opt zed objet_boite_zed sep sep objet_boite_zed end zed begin para_opt syntax objet_boite_zed sep sep objet_boite_zed end syntax para_opt tat tat enabled disabled d finition_ensemble_donn d finition_type_libre liste_identifiant identifiant branche branche 5 also objet_boite_zed d finition_ensemble_donn d finition type libre sep Pour en savoir plus sur la grammaire compl te du logiciel d ORA Canada veillez consulter 16 25 branche liste identifiant identifiant nom variable nom op d coration marque sym in sym pre sym post th or me usage nom th or me par formel g n pr dicat pr dicat 1 identifiant nom variable 1data expression rdata identifiant id
30. pzq proof use DefAltDeImplication1 use DefAltDeImplicationl p q q p with disabled implicationDef fauxDef prove use lemmel6 p p q q apply DoubleNegation to expression q simplify with disabled implicationDef fauxDef prove apply ouCommutativite to expression p V q simplify apply ouCommutativite to expression p V q simplify use lemmel6 p q q p use lemmel6 p q q p apply DoubleNegation to expression p simplify with disabled implicationDef fauxDef prove theorem antisymetrie Vp q BoolGries e p q q p p q vrai proof use DefAltDeImplication1 use DefAltDeImplicationl p q q p with disabled RegleDOr implicationDef etCommutativite etAssociativite ouAssociativite ouCommutativite DistOuSurEquiv2 DistOuSurEquiv1 DeMorgan1 DeMorgan2 DistOuSurEt1 DistEtSurOul DistNegSurEquiv1 equivAssociativitel TroisPointSoixanteQuinze prove apply DistEtSurOul to expression p V q q V p simplify apply etCommutativite to expression pV q A aq simplify apply etCommutativite to expression p V q p simplify 156 theorem antisymetrie suite de la preuve pr c dante Vp q BoolGries e p q q p p q vrai proof apply DistEtSurOul to expression q a pV q simplify apply DistEtSurOul to expression p p V q simplify apply Contradiction simplify use Contradiction p q apply DoubleNegation simplify apply ouldentitel
31. qui sont donn s par des labelled predicates qui ne sont pas trait s dans cette pr sente recherche Les trois commandes automatiques sont d finies ci dessous Voir 5 2 5 pour une explication br ve des labelled predicates 36 Simplify La syntaxe de cette premiere commande automatique est commande simplify trivial simplify Lors d une demande de simplification avec la commande simplify Z EVES r alise les op rations suivantes il fait du raisonnement au sujet de l galit au sujet des entiers et au sujet des propositions il v rifie si le but est une tautologie et il applique des r gles de transfert l usage frule et des r gles d hypoth se les th or mes d usage grule et les hypoth ses du but courant o cela est possible dans le but Cette commande est tr s utile en conjonction avec la commande use car elle permet d utiliser les r gles d hypoth se pour les appliquer au but sans faire appel aux r gles de r criture les th or mes d usage rule r gles qui souvent changent le but courant ce qui fait en sorte que l hypoth se n est plus utile La commande trivial simplify est moins puissante mais plus rapide que la commande simplify Cette commande r alise seulement une partie d une simplification Elle v rifie seulement les tautologies et elle r alise un raisonnement sur les propositions Rewrite La commande rewrite poss de cette syntaxe commande rewrite trivial rewrite prove by r
32. r ponse Vous verrez qu elle est plus compr hensible qu elle parait au premier abord Nous la d cortiquerons ensemble Tout d abord Z EVES nous annonce qul a bien re u et enregistr le th or me en marquant theorem DistNegSurEquiv4 theorem DistNegSurEquiv4 Ensuite le d monstrateur se met en position pour tre pr t d montrer ce th or me Beginning proof of DistNegSurEquiv4 p Mn BoolGries NN land q Nin BoolGries NN implies non p equiv q equiv non p q Ceci est notre but initial notre th or me N oubliez pas que lorsque Z EVES se met en position pour d montrer un th or me il ex cute pr ala blement la commande prenex pour enlever les quantificateurs universels Ensuite il affiche le th or me suivant la priorit des op rateurs il les af fiche de fa on ce que l on reconnaisse rapidement les diff rents pr dicats et comment ils sont reli s entre eux Pour continuer Z EVES accomplit la premi re commande donn e dans les directives pour r aliser la preuve la commande reduce Il ne mentionne pas la commande qu il effectue mais on voit tout ce qu elle fait r aliser au d monstrateur Voil la partie associ e la commande reduce Which simplifies when rewriting with DistNegSurEquivi DistNegSurEquiv2 forward chaining using KnownMember declarationPart knownMember internal items with the assumptions select _2 _1 select _2 _2 non declaration equiv declara
33. rences entre 80 d monstrateurs automatiques de th or mes grace aux crit res de comparaison nonc s la section 3 1 A 1 Plateformes langage de base et puissance maximale 84 plateforme Langage Puissance de base maximale Logique de premier ordre classique Logique classique Logique de premier ordre classique Logique de premier ordre classique Logique de premier ordre classique ACL2 Unix Windows 98 Macintosh CLIN CLIN S RDL lt U T o a amp 3 5 ct eo 5 gt i Z Prolog premier ordre constructive constructive ae Fle Logique classique N A Logique de premier ordre classique Logique de premier ordre Logique classique Logique de premier ordre classique Logique de premier ordre classique Fic A 1 Tableau sur les diff rences entre les d monstrateurs automatiques de th or mes suivant les criteres de comparaison plateforme langage de base et puissance maximale 85 plateforme Langage Puissance de base maximale FT HR Fic A 2 Tableau sur les diff rences entre les d monstrateurs automatiques de th or mes suivant les criteres de comparaison plateforme langage de base et puissance maximale suite 86 plateforme Langage Puissance de base maximale Windows ordre constructive Solaris ordre classique ordre classique ML constructive Prolog premier ordre ordre classique ordre classique Windows constructive et
34. s lectionnez la commande Run Normalement vous devriez voir le point d interrogation changer pour un Y pour dire que la commande a eu un effet sur le but courant Ensuite il faut entrer la deuxieme commande de la preuve manuellement comme vous venez de le faire pour la pr c dente sauf que vous crivez dans le mini editor la commande apply ouCommutativite to expression q ou p ou r Ensuite vous effectuez cette commande l aide de la commande Run Ceci vous donne le m me but courant qu la m me tape dans la preuve de ce lemme dans le mode textuel Finalement vous compl tez la preuve l aide de la commande rewrite accessible dans les commandes du bouton Reduction Le lemme lemme7 est prouv Revenez la fen tre Specification Normalement cette tape devant les th or mes lemme6 et lemme il devrait y avoir deux Y Si cela n est pas le cas revisez la s quence r alis e jusqu pr sent Vous tes maintenant pr ts prouver le th or me DistOuSurOul Acc dez la fen tre Proof de ce th or me Ensuite entrez manuellement et une la fois les commandes use lemme6 et use lemme7 de la m me mani re que celle utilis e jusqu pr sent dans le mode graphique Terminez la preuve en chois sissant la commande rewrite dans le bouton Reduction Retournez ensuite dans la fen tre Specification et votre th or me est d montr Cet exemple devrait vous avoir permis de mieux comprendre le fo
35. simplify 13 apply etldempotence to expression p ou q et p ou q 14 simplify 15 apply RegleDOr to expression p et q 16 simplify 17 apply equivCommutativitel to expression p ou q equiv p equiv q equiv p ou q 18 simplify 19 use equivAssociativitel p p equiv q q p ou q r p ou q 20 apply equividentite1 to expression p ou q equiv p ou q 21 simplify 22 with disabled ouAssociativite ouCommutativite prove La d monstration est plut t complexe mais elle est donn e pour montrer que Z EVES r ussit bien g rer les d monstrations longues 6 2 Exemples sur la th orie des ensembles Tout au long de cette recherche nous nous sommes attard s la d mon stration de th or mes selon la logique de Gries amp Schneider pour la logique propositionnelle Il existe aussi d autres th ories int ressantes et nous avons tent d en explorer quelques facettes avec Z EVES Nous nous sommes int ress s la th orie des ensembles Cette th orie est d j tr s bien implant e dans Z EVES alors nous avons r utilis les op rateurs d j pr sents dans le d monstrateur Notre but tait de r aliser des d monstrations de th or mes de la th orie des ensembles de Gries amp Schneider mais avec les axiomes de base de Z EVES Trois op rateurs taient inconnus du d monstrateur il a fallu les implanter Ces op rateurs sont le surensemble 2 le suremsemble propre 2 et le compl ment Pour le
36. uti liser dans la d monstration du th or me principal Commen ons tout d abord par prouver le premier lemme que nous appelerons lemme6 pour suivre la notation utilis e dans cette recherche Donnons Z EVES ce premier lemme begin theorem lemme6 forall p q r BoolGries p ou q ou r p ou p ou q Nou r end theorem Ensuite Z EVES est en position pour prouver ce lemme Tentons de le prouver par une commande simple rewrite car nous savons que ce th or me ne n cessite pas beaucoup d tapes et ces tapes devraient tre automatique dans Z EVES Entrons donc la commande rewrite Cette commande nous donne le but courant true Z EVES a donc d montr le th or me lemme6 avec nos r gles de r criture 23 lt Un lemme est un th or me de moindre importance utilis dans la preuve d un th or me auquel on s int resse davantage 4 24Ceci n est qu une suggestion de preuve Il en existe surement plusieurs mais c est celle ci que nous privil gierons 63 D montrons alors l autre partie et appelons la lemme7 Nous donnons tout d abord Z EVES le lemme pour qu il puisse se mettre en position pour la d monstration de celui ci begin theorem lemme7 forall p q r BoolGries p Nou p Vou q Nou r p Nou q Nou p Vou r end theorem Maintenant que Z EVES est pr t pour la d monstration de ce lemme donnons lui la premiere instruction Tentons tout d abord de voir ce que
37. vous venez de copier vous pouvez r aliser ceci gr ce la commande Paste dans le menu Edit de l interface textuel 6 Appuyez sur la touche entr e sur votre clavier juste devant la derni re instruction que vous venez de coller Ceci enclanchera Z EVES qui se mettra lire les informations et ex cuter les d monstrations 7 Attendez que le d monstrateur ait termin toutes ses d monstrations et ensuite la banque de donn es que vous d siriez sera charg e Mode graphique Charger la banque d axiomes et de th or mes dans le mode graphique est beaucoup plus rapide et simple que dans le mode textuel La m thode est presque identique pour charger toute la banque de donn es ou seulement une partie de celle ci En fait elle ne diff re que par la derni re tape vrai dire la raison pour laquelle le chargement des th or mes est beaucoup moins long dans le mode graphique que dans celui textuel est le fait que le mode graphique ne donne que les th or mes sans v rifier ni prendre en consid ration les preuves de ceux ci Donc cela revient presqu dire que tous les th oremes sont rendus des axiomes car ils n ont pas de preuves dans le mode graphique mais ce ne sont pas des axiomes car on peut prouver chacun des th oremes avec les axiomes qu on a La m thode commune pour acc der en partie ou en totalit la banque d axiomes et de th or mes dans le mode graphique est la suivante 56 1 Ouvrez Z EVES dans l
38. 7 avec p p V q V p V r p 61 Nous avons r ussi d montrer ce th or me Donc c est un th or me dans notre systeme d axiomes Voyons comment Z EVES se d brouille pour r aliser la d monstration de ce th or me Mode textuel Pour d buter il faut d abord donner Z EVES les diff rents th or mes et axiomes pr c dant celui que nous d sirons d montrer Donc ditons le fichier AlgBoolZLa TeX zed et copions dans le presse papier du syst me d ex ploitation les informations pr c dant le Jemme6 nous ne copions pas les th or mes lemme6 et lemme car nous devrons les cr er dans la d monstra tion Ensuite d marrons Z EVES en mode Z PTEX Les tapes suivre pour r aliser ceci sont d crites dans la section 5 2 9 Pla ons les informations dans la fen tre de Z EVES et appuyons sur entr e devant la derniere ligne d ins truction apparaissant l cran Attendons quelques instants Maintenant que nous avons tous nos outils nous pouvons travailler Tout d abord il faut entrer le th or me que nous d sirons prouver dans notre cas le th or me DistOuSurOul1 Nous le d finissons comme ceci begin theorem DistOuSurOui forall p q r BoolGries p ou q ou r p ou q ou p ou r end theorem Ensuite Z EVES se met en place pour la d monstration du th or me V rifions tout d abord si l aide des axiomes Z EVES serait capable de d montrer le th or me sans notre aide
39. BoolGries p V p vrai vrai dire cette commande cr e un effet sp cial dans Z EVES L application de prenex fait en sorte que chaque variable li e devient libre par la suite Les substitutions sont faciles r aliser par la suite 39 5 2 6 4 Utilisation des galit s Il n existe qu une commande qui permet d utiliser les galit s Equality substitute La commande a la syntaxe suivante commande equality substitute expression Si une expression e est sp cifi e dans la commande et qu il y a une hypoth se dans le but courant qui donne une galit entre e et une expression e alors toutes les occurrences de e dans le but sont remplac es par e l expression voulue Si aucune expression e n est sp cifi e alors les hypoth ses contenant des galit s entre expressions s il y en a sont choisies gr ce une m thode heuristique et les remplacements sont r alis s dans le but courant 5 2 6 5 Modificateurs Il y a quelques commandes qui permettent d affecter le comportement d une commande de r duction de fagon temporaire Celles ci sont d finies ci dessous With disabled Ce modificateur a la syntaxe suivante commande with disabled liste nom v nement com mande liste nom v nement nom v nement nom v nement nom v nement d claration nom r gle de transfert nom r gle de r criture nom r gle d hypoth se nom d finition La commande with
40. Grace aux crit res de comparaison nonc s la section 3 1 nous avons pu proc der l valuation des d monstrateurs automatiques de th or mes Cette valuation a permis d liminer plusieurs d monstrateurs et de cibler rapidement les plus int ressants parmi la liste Ceci a permis de s lectionner cinq de ces d monstrateurs pour les approfondir Ces d monstrateurs auto matiques de th or mes sont e ACL2 HOL98 HOL Light e Otter e Z EVES Pour le restant de ce chapitre le terme Unix d signe autant cette plateforme que celles fonctionnant sur le m me principe que ce syst me d exploitation Par exemple ce terme r f re aussi Linux Solaris DEC Unix IRIX SCO Unix 11 4 1 ACL2 Le d monstrateur automatique de th or mes nomm ACL2 6 est un lo giciel tr s int ressant programm en Common Lisp Ses principaux avantages et d savantages sont r unis ici Avantages 1 Il est assez polyvalent il tourne sur des machines ayant comme syst me d exploitation Unix Windows 98 et Mac OS 2 La documentation concernant ce logiciel est tr s complete environ 900 pages 3 Il ne n cessite qu un compilateur de Lisp pour fonctionner 4 Le logiciel est gratuit 5 Ce logiciel traite de la th orie des ensembles finis D savantages 1 Il est difficile t l charger pour une personne d sirant une copie du logiciel adapt e une machine ne fonctionnant pas sur la plateforme Unix
41. Gries NN implies non p equiv q equiv non p q Which simplifies when rewriting with DistNegSurEquivi DistNegSurEquiv2 forward chaining using KnownMember declarationPart knownMember internal items with the assumptions select _2 _1 select _2 _2 49 non declaration equiv declaration internal items to p in BoolGries land q in BoolGries implies non p equiv q equiv Non p q Applying equivCommutativitel to Anon p equiv q gives p Mn BoolGries NN land q Nin BoolGries NN implies IF non p in BoolGries land q in BoolGries THEN q equiv non p ELSE non p equiv q equiv non p Which simplifies forward chaining using KnownMember declarationPart knownMember internal items with the assumptions select _2 _1 select _2 _2 non declaration equiv declaration internal items to p in BoolGries land q in BoolGries implies IF non p in BoolGries THEN q equiv non p equiv non p ELSE non p equiv q equiv non p Which simplifies when rewriting with equivCommutativite3 applicationInDeclaredRangeFun inPowerSelf forward chaining using KnownMember declarationPart knownMember internal items with the assumptions select _2 _1 select _2 _2 equiv declaration fun _type non declaration internal items to true Il Ja q 50 Avant de prendre peur prenez quelques instants pour bien d cortiquer cette
42. Les d monstrateurs automatiques de th oremes Claude Bolduc 24 aout 2001 Cette recherche a pu tre men e terme gr ce A une bourse CRSNG du 1 cycle Table des mati res 1 I Introduction d Motivation d m a 1054 94 ENSE X Zw feed ome ENS 1 2 Pr sentation du projet 5 12 a beoe eR Seq Quatre vingt diff rents d monstrateurs automa tiques de th or mes 2 I 5 D monstrateur automatique de th or mes choisi Z EVES La logique propositionnelle 2 1 Introduction la logique propositionnelle 2 2 La syntaxe de la logique propositionnelle Les diff rents d monstrateurs automatiques de th or mes 3 1 Les crit res de comparaison 3 2 Les d monstrateurs v rifi s Les d monstrateurs automatiques de th or mes qui ont t approfondis Zd oA Lote 0 PUE Ae ID RN Ker ee Sat BEAR E RSE 2 122 STOLE OS ee r0 uera eet ar PUT eae ele tte a T9 HAO LIB SE he ge doa dra ae Rhe use a et to c dd OUR oo Loco ed ios ded da ergo ded eraa ene e 45 SEES ee eth ne wie ew depu iere c Oe RS HN Z EVES Version 2 1 16 17 5 1 Raisons qui motivent le choix de ce d monstrateur 17 5 LI HOLS sn ue ne Mee eve de Os os MA Ye nue 17 Bs ZV EVES e ose deat pA age RISRASER Reds 18 5 2 Guide d utilisation de Z EVES Version 2 1 19 DHAL Introductions 3 ro Ide dede BRE S rie 19 5 2 2 Obtenir et installer Z E
43. S et que les occurrences de S sont remplac es par la d finition de S mais o chacune des variables de cette d finition sont maintenant d cor es Pour viter ce probleme on utilise la commande invoke predicate S qui permet de transformer seulement les occurrences de S dans le but courant Use La syntaxe de la commande est donn e comme suit 12D apr s le Z standard 19 un sch ma sans d coration repr sente l tat initial du sch ma tandis qu un sch ma d cor du signe prime repr sente l tat final du sch ma 34 use r f rence th or me nom th o d coration par eff g n remplace commande r f rence th or me ments nom th o i mot remplacements renommer ou subst renommer ou subst renommer ou subst nom d cl nom d cl nom d cl expression nom d cl identifiant nom op La commande use sert prendre un th or me d j existant et le rajouter dans les hypoth ses du but courant Cela sert surtout si le th or me que l on souhaite ajouter est un th or me qui n a pas t d fini avec un usage les usages sont d finis dans Z EVES comme tant axiom rule frule ou grule mais cette commande s applique aussi tr s bien aux th or mes d finis avec un usage Le nom du th or me doit tre crit correctement at tention Z EVES est sensible la casse pour les noms de th or mes avec sa d coration s il y a lieu Si le th or me comporte des pa
44. SurEquiv2 to expression r V p q p V q simplify apply DistOuSurEquiv2 to expression r V p q simplify apply ouCommutativite to expression r V p simplify apply ouCommutativite to expression r V q simplify apply ouCommutativite to expression r V p V q simplify use equivA ssociativitel p p q pV d r7 pVr aVvr r pV qV r rewrite theorem lemme9 Vp q r BoolGriesep qA r p q r qVr pVr pV avr proof rewrite II S lt RQ II theorem lemme10 Vp q r BoolGriesep q pV q r plVr qVr pVaVr p q r qVr pVq pVr pVqvVr proof rewrite Fin de l ajout de lemmes 129 theorem rule etAssociativite Vp q r BoolGries ep qN r p q r proof use lemme8 use lemme9 use lemme10 with disabled RegleDOr etCommutativite ouCommutativite ouAssociativite ouldempotence DistOuSurEquiv1 equivCommutativitel equivAssociativitel equivAssociativite2 equivCommutativite3 rewrite theorem rule etIdempotence Vp BoolGries ep p p proof rewrite theorem etIdempotence2 Vp BoolGries e p p p proof rewrite theorem rule etIdentitel Vp BoolGries e p vrai p proof rewrite theorem rule etIdentite2 Vp BoolGries e vrai p p proof rewrite theorem etIdentite3 Vp BoolGries e p p vrai proof rewrite 130 theorem etIdentite4 Vp BoolGries e p vrai p proof rewrite theorem rule ZeroDeEt1 V p BoolGries e p faux faux proof with disabled fauxDef rewrite theorem rule Ze
45. VES 19 5 2 3 D buter le d monstrateur 20 5 24 Explication des interfaces 21 5 2 5 Syntaxe du d monstrateur 24 5 2 6 Commandes du d monstrateur 30 5 2 7 Formalisme des donn es d entr e 43 5 2 8 Formalisme des donn es de sortie 49 5 2 9 Utilisation de la banque d axiomes et de th or mes 54 5 2 10 Exemple complet d une d monstration de th or me 61 5 2 11 Sp cialisation du d monstrateur 68 6 Exemples d j test s 72 6 1 Exemples sur la logique propositionnelle 73 6 2 Exemples sur la th orie des ensembles 77 7 Conclusion 80 III Annexes 83 A Annexe Diff rences entre 80 d monstrateurs automatiques de th or mes grace aux crit res de comparaison nonc s la section 3 1 84 A 1 Plateformes langage de base et puissance maximale 84 A 2 Qualit de la bibliographie et type d interaction 90 A 3 Co t de implantation 53 td OE ox nq eure ue rra 96 A 4 Rapidit avec d monstration complexe et simple convivialit et niveau IBEGIOE dete d dae po reed a ne e pe 102 A 5 Adresses Internet a bas Sok e Bee Ge rU SES 108 B Annexe Axiomes implant s dans Z EVES pour la cr ation de l alg bre bool enne 114 il C Annexe Th or mes test s dans Z EVES ainsi que leur preuve respective 119 iii Table des figures Zl 5
46. VL Un compilateur Common Lisp Nathm the Boyer Un compilateur Moore prover Common Lisp dans le cadre d une utilisation acad mique ou de recherche Rien gratuit car on ne peut que l utiliser sur le web Fic A 13 Tableau sur les diff rences entre les d monstrateurs automa tiques de th or mes suivant le crit re de comparaison co t de l implantation suite 99 Co t de l implantation Un compilateur C Un compilateur Prolog Le logiciel Objective Les logiciels Emacs gratuit Tcl Tk LaTeX gratuit Fic A 14 Tableau sur les diff rences entre les d monstrateurs automa tiques de th or mes suivant le crit re de comparaison co t de l implantation suite 100 Co t de l implantation SCOTT combinaison Un compilateur C d Otter et de FINDER il SETHEO ien gratuit Simplify ti Sun s JDK ou JRE gratuit Logiciel non disponible SPASS Rien gratuit mais le code source n est pas fourni pour Windows SPRFN i prolog SPTHEO Logiciel non disponible Theorema Logiciel non disponible mais on peut utiliser une version incompl te sur le web TPS i Common Lisp gratuit Typelab Logiciel non disponible Watson Le logiciel Standard ML gratuit Yarrow Un compilateur Haskell Z EVES i Fic A 15 Tableau sur les diff rences entre les d monstrateurs automa tiques de th or mes suivant le crit re de comparaison co t de l implantation suite 101 A 4 Rapidit avec
47. Vp q BoolGries ep q gt p V q vrai proof prove use DistOuSurEquiv2 r p V q use lemme14 simplify apply equivIdentitelto expression p V q p V q simplify prove 150 theorem Affaiblissement4 Vp q r BoolGries e p V q r gt pV q vrai proof with disabled DistOuSurEquiv1 prove apply ouCommutativite to expression q V p V q V r simplify apply ouCommutativite to expression p V q V r simplify apply ouAssociativite to expression q V r V p simplify apply ouCommutativite to expression q V r V p simplify apply ouAssociativite to expression r V p V qV q simplify apply ouldempotence to expression q V q simplify apply ouCommutativite to expression r V p V q simplify apply ouCommutativite to expression r V p simplify use equivIdentitel p p V qV pV r with disabled ouAssociativite ouCommutativite equivAssociativitel equivCommutativitel equivCommutativite3 DistOuSurEquiv 1 DistOuSurEquiv2 prove Ajout de lemmes theorem lemme20 Vp q r BoolGries ep qNrT p q r proof with disabled RegleDOr prove theorem lemme21 Vp q r BoolGriesepV qV r pVqvr proof prove 151 theorem lemme22 Vp q r BoolGries ep qV r p gt q V p r proof use DefAltDeImplicationl g q V rl use DefAltDeImplicationl use DefAltDelmplication1 q r use DistOuSurOul p p with disabled implicationDef ouCommutativite ouAssociativite DeMorgan1 DeMorgan2 prove Fin de l ajout de lemmes
48. aire un g teau totalement identique celui que vous lui pr sentez Ce g teau est la m me chose qu un th or me Votre apprenti utilisera ses connaissances et ses ingr dients pour essayer de faire ce magnifique g teau seul mais il se peut qu il en soit incapable ce moment l vous devez lui donner des indices comme utiliser tel ou tel ingr dient avec telle quantit ou simplement lui dire de ne pas se servir de tel ingr dient De la m me mani re vous pouvez dire votre d monstrateur de tenter de d montrer un th oreme et s il n y arrive pas seul vous pouvez lui donner des commandes sp cifiques pour le diriger afin qu il r ussisse cette t che Dans cette recherche nous donnerons pour d buter notre apprenti cuisinier seulement des axiomes de la logique quationnelle de Gries amp Schneider pour v rifier comment il se d brouille avec ces ingr dients En bref la logique propositionnelle est une repr sentation simplifi e de la r alit qui nous permet de mieux isoler un probl me pour d terminer sa v racit 2 2 La syntaxe de la logique propositionnelle La logique propositionnelle possede sa propre notation D ailleurs celle ci varie quelque peu d un ouvrage un autre La syntaxe utilis e dans cette recherche est celle pr conis e par Gries amp Schneider 5 Cette notation se compose des conventions de base donn es dans la figure 2 1 Cette notation permet de repr senter des phrases franca
49. al Toolkit 17 Normalement ceci ne sera pas n cessaire car Z EVES poss de un tr s bon niveau d automatisme dans les preuves de la th orie des ensembles avec ses propres axiomes 79 Chapitre 7 Conclusion En r sum les d monstrateurs automatiques de th or mes de la logique classique de premier ordre sont extr mement int ressants pour apprendre la d monstration de th oremes Nous avons r alis dans cette recherche un tour d horizon des diff rents d monstrateurs automatiques de th or mes existants et nous avons approfondi et test un de ceux ci Z EVES version 2 1 Nous lui avons implant la logique quationnelle de Gries amp Schneider pour v rifier son comportement avec cette logique Le d monstrateur a tr s bien r pondu cette implantation et nous avons m me cr une bauche de la th orie des ensembles Nous avons donc r ussi implanter la logique que nous vou lions dans Z EVES dans le but de favoriser un apprentissage rapide de la d monstration de th oremes Dans ce rapport on ne s est int ress qu aux d monstrateurs automa tiques de th or mes de la logique classique de premier ordre Pourtant il y a d autres d monstrateurs fonctionnant sur d autres logiques qui sont aussi int ressants Prenons le cas d OSCAR un d monstrateur automatique de th or mes qui a t d velopp l universit de Il Arizona C est un d monstra teur automatique de th or mes qui raisonne sur des
50. angements complexes en met tant en relation des variables bool ennes Les op rateurs de coordination per Une proposition est un nonc qui peut tre vrai ou faux 4 mettant de r aliser des arrangements complexes sont d finis dans la section 2 2 Cette logique est bas e sur des axiomes de base pour la liste exhaustive de ceux utilis s dans cette recherche voir 5 Un axiome est une expression dont on assume qu elle est un th or me sans en donner la d monstration 4 Ces axiomes permettent de d river des th or mes Un th or me est soit un axiome soit la conclusion d une r gle dont les pr misses sont des th or mes ou soit une expression dont on d montre qu elle est gale un axiome ou un th or me pr c demment d montr 4 La logique quationnelle de Gries amp Schneider est bas e seulement sur des axiomes qui sont des tautologies Chaque th or me de la logique propositionnelle peut tre d montr l aide des axiomes de cette logique Il y a plusieurs fa ons de r aliser une preuve d un th or me Il y a donc plusieurs mani res d arriver au r sultat Une facon de proc der peut faire en sorte que l on arrive tr s rapidement et de fa on efficace au r sultat alors qu une autre m thode pourrait rallonger de beaucoup la preuve et m me ne pas y parvenir Les humains sont capables de produire des preuves tres courtes en usant d intelligence et d exp rienc
51. apply ouCommutativite to expression p V q simplify use TroisPointQuaranteDeux2 p q q p apply DoubleNegation to expression p simplify apply DistNegSurEquiv2 to expression 5 q q V p simplify prove theorem TroisPointCinquanteNeuf2 Vp q BoolGriesep q p qzsp proof use TroisPointCinquanteNeuf 1 use ModificationTheo p p q2 p q q p use ModificationTheo p p qq p q p with disabled RegleDOr etCommutativite etAssociativite prove theorem TroisPointSoixante Vp q r BoolGriesep qr p qsmp rzp proof prove theorem TroisPointSoixanteEtUn Vp q BoolGriesep qp p 4q proof use TroisPointSoirantelr p prove Ajout de lemme theorem lemme15 Vp q r BoolGries e p q r q proof prove II S II 3 137 Fin de l ajout de lemme theorem Remplacement Vp q r BoolGries e p q r 2 p 2 p 4 r2 q proof prove apply equivCommvutativitel to expression q V r p pV q simplify apply equivCommutativitel to expression p V q p q qV r simplify apply equivCommutativitel to expression p q simplify use lemmel5 p r pVrr p gVr pV q use equivCommutativitel p q V r q p V q prove Ajout de lemme theorem lemme16 Vp q BoolGries e 5 q V p V q vrai proof apply ouCommutativite to expression q V p V q rewrite Fin de l ajout de lemme 138 theorem equivDef Vp q BoolGriesepzq p q V op oq proof appl
52. axe pr sent e dans la section 5 2 5 syndef coeur infun5 coeur Ensuite nous devons d clarer son type dans une d finition d axiome g n rique begin axdef _ coeur V BoolGries cross BoolGries fun BoolGries end axdef Maintenant il ne reste qu a entrer les axiomes de cet op rateur L associativit de Q begin theorem rule coeurAssociativite forall p q r BoolGries p coeur q coeur r p coeur q coeur r end theorem La commutativit de Q begin theorem rule coeurCommutativite 68 forall p q BoolGries p Ncoeur q q coeur p end theorem La distributivit de sur begin theorem rule DistCoeurSurEquiv forall p q r BoolGries p coeur q equiv r non p coeur q equiv p coeur r end theorem Notre nouvel op rateur est donc fonctionnel De plus notre logique vient d tre tendue Une autre fa on d tendre la logique implant e dans cette recherche est de donner de nouvelles constantes au type l ensemble BoolGries Bien entendu il faut aussi donner Z EVES les axiomes qui d crivent le compor tement de ces nouvelles constantes De cette fa on nous pouvons obtenir une logique qui n est plus simplement deux valeurs vrai et faux mais elle peut aussi avoir d autres possibilit s Par exemple si nous souhaitons introduire deux nouvelles constantes ap pell es peut tre1 et peut tre2 alors il faut d abord d clarer ces cons
53. car il n y a pas d instructions sur l installation sur une plateforme autre que Unix 2 Il prend 19 5 Mo de m moire 3 Il est simplement un d monstrateur de th or mes semi automatique il fonctionne seulement par dialogue Il demande beaucoup de temps d apprentissage pour bien savoir s en servir quelques mois pour un bon informaticien d apr s son cr ateur La documentation concernant la th orie des ensembles finis est dis pers e l int rieur du code 4 2 HOL98 Le d monstrateur automatique de th or mes HOL98 20 est un logiciel crit en Moscow ML d montrant des th or mes de la logique classique Avantages de HOL98 12 Il est adapt pour les plateformes Unix et Windows NT Sa bibliographie est tr s compl te et int ressante il y a trois manuels sur son utilisation qui se compl tent le tutoriel 10 les r f rences 9 et la description 8 de HOL La notation de la logique dans ce logiciel est proche de la notation utilis e par Gries amp Schneider Le style de preuve est relativement facile suivre 5 Ce logiciel est gratuit Ce logiciel traite de la th orie des ensembles D savantages de HOL98 1 L installation de Moscow ML est assez complexe celle de HOL98 aussi si on utilise une autre plateforme que Windows NT L utilisation de HOL98 n est pas tr s intinctive pour un nouvel utilisa teur Son mode d interaction est le dialogue 4 C est un d m
54. cas g n raux avec en son sein un agent rationnel de d duction C est un d monstrateur exp rimental tr s puissant qui permet d aider dans les recherches en philosophie 80 Bibliographie 10 11 12 Le Nouveau Petit Robert Maury Imprimeur S A 1993 ORA Canada ORA Canada EVES Verification System ORA Canada 1999 http www ora on ca eves html Office de la langue fran aise Le grand dictionnaire terminologique Adresse URL http www granddictionnaire com fs global 01 htm 2001 Jules Desharnais Notes de cours du cours de logique et structures discr tes D partement d informatique Universit Laval 2000 David Gries et Fred B Schneider A Logical Approch to Discrete Math Springer 1994 Matt Kaufmann et J Strother Moore ACL2 version 2 5 Universit du Texas Austin 2000 http www cs utexas edu users moore acl2 acl2 doc html Melvin Fitting First Order Logic and Automated Theorem Proving Springer 1996 Mike Gordon The HOL System Description Cambridge Research Cen ter of SRI International f vrier 2001 Mike Gordon The HOL System Reference Cambridge Research Center of SRI International f vrier 2001 Mike Gordon The HOL System Tutorial Cambridge Research Center of SRI International f vrier 2001 John Harrison HOL Light Universit de Cambridge 1998 http www cl cam ac uk users jrh hol light John Harrison The HOL Light Manual 1 1 University of Camb
55. ce non d cl_basique d cl_basique liste noms d clar s type nom d cl nom d cl identifiant nom op BoolGries N Z autre ensemble donn Fic 5 2 Grammaire utilis e pour la formation des pr dicats 45 Yp q BoolGries p p q q Pourtant ce simple th or me se d montre ce stade ci dans la progression suivie par Gries amp Schneider Donc nous avons d tre vigilant pour ne pas oublier tous les cas possibles Dans le mode textuel il tait tr s facile de transcrire ces axiomes en sui vant la syntaxe donn e la section 5 2 5 Nous avons utilis l environnement fourni pour la conception de th or mes et nous avons donn comme usage chacun des axiomes rule Ce qui d signait cet axiome comme tant une r gle de r criture que Z EVES allait utiliser automatiquement pour r aliser des preuves De plus nous ne donnions pas de preuve des axiomes un axiome est un th or me que l on accepte comme tant vrai d apr s notre d finition de ce terme Voil un exemple du code utilis dans le mode textuel pour implanter l axiome nonequivDef Vaxiome 3 13 d apr s la num rotation des th or mes du cours Logique et Structures Discr tes 4 begin theorem rule nonequivDef forall p q BoolGries p nonequiv q non p equiv q end theorem Comment entrer un th or me Les th or mes sont donn s de la m me fa on que les axiomes pr sent s auparavant
56. ction alors il faut utiliser la commande use ouAssociativite2 q p r q1 Cette commande ajoute dans les hypoth ses p BoolGries p BoolGries q BoolGries gt pV pV q pVvpV q On doit absolument utiliser la commande use pour se servir du th or me ouAssociativite2 car il a t d fini sans qu on lui donne d usage Autre chose int ressante que la commande use r alise avant de faire la substitution ou de renommer une variable Z EVES prend chaque quantifi cateur universel et l enl ve pour rendre chacune des variables du th or me libre Pour combler la lacune caus e par l enl vement de ces quantificateurs il ajoute aux hypoth ses du th or me que chacune des variables qui taient li es au d part est maintenant l ment de l ensemble le type qu on lui avait sp cifi 5 2 6 2 2 La maniere automatique Les commandes automatiques pour la d monstration de th or mes dans Z EVES sont au nombre de trois au m me titre que celles de la maniere manuelle Ces trois op rations sont des commandes de r duction que le d monstrateur effectue pour r duire un but une forme quivalente qu il consid re plus simple pour lui Attention les commandes automatiques n utilisent que les th or mes qui ont un tat actif enabled Un th or me est consid r actif par Z EVES d s que celui ci est v rifi et accept syn taxiquement Les seuls th or mes qui peuvent tre inactifs disabled sont ceux
57. ction de type dialogue Le style de preuve est tr s peu explicite sur les transformations ef fectu es 15 Deuxieme partie Z EVES Chapitre 5 D monstrateur automatique de th or mes choisi Z EVES Version 2 1 5 1 Raisons qui motivent le choix de ce d monstrateur Apr s une analyse approfondie des cinq d monstrateurs automatiques de th or mes deux choix ont t retenus HOL98 et Z EVES Ces deux logiciels ont t test s d une facon rigoureuse pour d terminer le meilleur choix entre ces deux d monstrateurs tout aussi int ressants l un que l autre L apprentissage de ces deux logiciels a t r alis et on a tent d implanter dans chacun de ces d monstrateurs la logique de Gries amp Schneider Cette exp rience a permis de faire ressortir les points suivants 5 1 1 HOL Avantages e Il poss de une librairie bool enne qu on peut utiliser pour r aliser une logique qui se rapproche de celle de Gries amp Schneider 17 e On peut modifier assez facilement les op rateurs d j pr sents et leur priorit et m me en d finir d autres D savantages e Il est difficile d apprentissage e Il ne poss de pas l quivalence comme op rateur e L interface est purement textuelle 5 1 2 Z EVES Avantages e L interface est graphique GUI ou textuelle e Z EVES est relativement facile d apprentissage la grammaire est faci lement accessible e Z EVES poss de l quivalence co
58. d un th or me le th or me Absorption1 avec sa preuve begin theorem Absorption1 forall p q BoolGries p Vet p ou q p proof rewrite apply DistOuSurEquiv2 to expression p ou q equiv p ou q simplify use ouAssociativite2 q p r q rewrite end theorem Vous pouvez aussi entrer un th or me sans nom dans l interface Z ATEX en utilisant simplement la commande try Cette commande poss de la syn taxe suivante commande try pr dicat Mode graphique Le mode graphique est identique au mode textuel pour la th orie de l implantation de l alg bre bool enne Ce qui diff re est la mani re d entrer les axiomes et les th oremes Comment entrer un axiome En suivant les r gles nonc es dans la section du mode textuel on a entr les axiomes en suivant la syntaxe suivante 1 Le num ro 3 55 dans la num rotation des th or mes utilis e dans le cours Logique et Structures Discr tes 4 20Les axiomes doivent tre entr s sans se soucier de la police de caract res Z EVES ne traite qu une criture italique 47 theorem rule nom th or me pr dicat Ce qui donne exactement le m me r sultat que dans le mode textuel Voici un exemple d un tel axiome dans le mode graphique l axiome no nequivDef le m me axiome que donn dans le mode textuel pour que vous puissiez voir la diff rence theorem rule nonequivDef Vp q BoolGries e p nonequiv
59. donnez vous m me comme notre type BoolGries Dans cette recherche vous pou vez remarquer que chaque variable est d clar e de type BoolGries Atten tion n oubliez pas que Z EVES d sire avoir comme th or me un pr dicat Donc chacun de nos axiomes a t mis sous forme d un pr dicat pour que le d monstrateur les accepte Ces pr dicats sont tous de la m me forme ils poss dent un quantificateur universel qui permet de d clarer chacune des variables de l axiome Ensuite il faut donner le corps de l axiome le pr dicat N oubliez pas que les op rateurs que nous avons implant s ne permettent que de cr er des expressions dans le langage de Z EVES Il y a plusieurs fa ons de r aliser un pr dicat voir 16 pour une liste exhaustive des diverses m thodes de cr ation de pr dicats la figure 5 2 vous retrouverez une partie de la grammaire de Z EVES que nous avons modifi e pour cr er nos pr dicats En regardant ceci nous nous rendons compte que nous devons relier au moins deux expressions par un op rateur de relation pour cr er un pr dicat celui qui a t choisi dans la pr sente recherche est l op rateur Nous avons donc d cr er notre alg bre bool enne en prenant ce facteur en compte Remarquez que chaque axiome poss de un op rateur de relation Ce facteur a compliqu quelque peu notre recherche car il fallait quel quefois donner plusieurs fois un axiome mais avec une forme diff rente pour pe
60. e apply equivCommutativitel to expression q q simplify use TroisPointDixzHuitl p q with disabled fauxDef rewrite theorem TroisPointQuaranteDeux2 Vp q BoolGriesep V q pV73q p proof use TroisPointQuaranteDeux1 use ModificationTheo p p V q2 pV 4q q p use ModificationTheo p p V q q 2 p V q 2 p prove by reduce theorem TroisPointQuaranteDeux3 Vp q BoolGriesep V q p pV 74q proof use TroisPointQuaranteDeux1 use ModificationTheo p p V q2 pV 4q q p use ModificationTheo p p V q2 p q p V q prove by reduce theorem TroisPointQuaranteDeux4 Vp q BoolGriesep V 7Aq pV q p proof use TroisPointQuaranteDeux3 prove 127 Th or mes de la conjonction theorem RegleDOr2 Vp q BoolGriesep q p ad DV a proof use ModificationTheo p p q q 2 p 2 q use ModificationTheo p p q p q q rewrite apply equivIdentitel to expression p p rewrite theorem RegleDOr3 Vp q BoolGriesep q p ad DV a proof use ModificationTheo p p q q p 2 q use ModificationTheo p p q2 pz q q rewrite apply equivIdentitel to expression p p rewrite theorem rule etCommutativite Vp q BoolGriesep q qA p proof reduce Ajout de lemmes 128 theorem lemme8 Vp q r BoolGriesep gAr p q pVq r pVr qVr pVaqavr proof apply RegleDOr to expression p q simplify apply RegleDOr to expression p q pVq Ar simplify apply ouCommutativite to expression p q pVq Vr simplify apply DistOu
61. e souvent m me d astuce Les d monstrateurs automatiques de th or mes essaient d imiter d une facon limit e le comportement humain lors de la d monstration de th o r mes Ces outils ont commenc par utiliser des heuristiques simples de d monstration de th or mes Ensuite ils se sont raffin s pour devenir plus performants et conviviaux La presque totalit des d monstrateurs automa tiques de th or mes performants ne sont pas totalement automatiques En fait pour augmenter leur puissance on les rend semi automatiques pour qu un humain puisse diriger le d monstrateur sa guise Cela occasionne aussi le fait que l humain doit souvent aider le d monstrateur En fait un d monstrateur automatique de th or mes est un peu comme Proposition complexe qui reste vraie en vertu de sa forme seule quelle que soit la valeur de v rit des propositions qui la composent 1 3 M thode de recherche empirique ayant recours aux essais et erreurs pour la r solution de probl mes 3 un apprenti cuisinier Vous vous tes les maitres cuisiniers Vous donnez votre l ve des ingr dients dont il doit se servir pour cuisiner des plats sp cifiques que vous d sirez Ces ingr dients sont les axiomes de base que votre d monstrateur connait Ensuite vous lui donnez un g teau d j pr par et d cor Il est d j tout pr t mais votre l ve n a rien vu de sa pr paration Vous dites votre apprenti de f
62. e 64 do aed TE CAMERE CY AE Bee A 15 Tableau sur les diff rences entre les d monstrateurs automa tiques de th or mes suivant le crit re de comparaison cott de l implantation suite usus ee EREMO ROSA eae A 16 Tableau sur les diff rences entre les d monstrateurs automa tiques de th or mes suivant les criteres de comparaison ra pidit avec d monstration complexe et simple convivialit et niveau d int r t sh A 17 Tableau sur les diff rences entre les d monstrateurs automa tiques de th or mes suivant les criteres de comparaison ra pidit avec d monstration complexe et simple convivialit et niveau d int r t stille e o ren xem So ES A 18 Tableau sur les diff rences entre les d monstrateurs automa tiques de th or mes suivant les crit res de comparaison ra pidit avec d monstration complexe et simple convivialit et niveau d int r t eultie s caos wa a iu RA RO SEU EOS A 19 Tableau sur les diff rences entre les d monstrateurs automa tiques de th or mes suivant les criteres de comparaison ra pidit avec d monstration complexe et simple convivialit et niveau d int r t suites ns cox RR ERA A 20 Tableau sur les diff rences entre les d monstrateurs automa tiques de th or mes suivant les criteres de comparaison ra pidit avec d monstration complexe et simple convivialit et niveau d int r t suite eee A 21 Adresses Internet utilis
63. e d monstrateur Cette banque d exemples est disponible dans le fichier SetTheoryZEVES zed Nous pouvons y acc der de la m me mani re que celle que nous avons utilis e pour notre alg bre bool enne dans la section 5 2 9 Nous pouvons donc utiliser facilement des d monstrations de cette banque d exemples et m me ajouter des th or mes de la th orie des ensembles grace aux op rateurs que nous avons implant s L ensemble X est un param tre formel g n rique 78 La manipulation de ce fichier est la m me que celle pour le fichier Alg BoolZLaTeX zed Quelques petites choses diff rent par contre dans le fi chier de la th orie des ensembles les d monstrations sont r alis es grace aux th or mes d j pr sents dans notre d monstrateur De plus le type Bool Gries n est plus utilis pour soumettre les th or mes Z EVES et nous utilisons maintenant un param tre formel g n rique nous l avons appel X dans cette recherche qui permet de rendre les th or mes portatifs tous les types que nous d sirons Nous n avons qu pr ciser lors de l utilisation d un th or me dans une preuve d un autre th or me que le param tre effectif g n rique sera le type utilis l int rieur de notre th or mef Avec tout ceci nous avons une bonne banque d exemples que nous pou vons utiliser et de plus nous pouvons la modifier facilement Les th or mes pr sents dans Z EVES sont disponibles dans le Mathematic
64. e expliqu e et n incluent jamais toutes les tapes d une d monstration Nous entendons donc r aliser un exemple complet pour permettre une bonne compr hension g n rale du d monstrateur automatique de th or mes Prenons un th or me simple mais int ressant dans sa d monstration et r alisons cet exemple dans les deux modes pour montrer les diff rences Le th or me choisi est le th or me DistOuSurOul Vp q r BoolGriesep V qVr pVq V pV r Avant m me de nous lancer dans l aventure p rilleuse de d montrer ce th or me il est bon d avoir une id e de la preuve Z EVES a un bon degr d automatisme mais il n cessite tout de m me notre aide de temps autre Tentons donc de d montrer ce th or me par nous m me Vp q r BoolGries ep V q V r Z p V q V p V r Idempotence de la disjonction 3 34 Vp q r BoolGries e p V p V q V is pVq V pVr Associativit de la disjonction 3 33 avec q r p qu Vp q r BoolGriesep V pV qVr S pVq V pV r Associativit de la disjonction 3 33 Vp q r BoolGriesep V pVq Vr pVq V pV r Commutativit de la disjonction 3 32 Vp q r BoolGriesep V qVp Vr pVq V pV r Associativit de la disjonction 3 33 avec p q q p Vp q r BoolGriesep V qV pVr S pVq V pV r Associativit de la disjonction 3 33 avec r p V r Vp q r BoolGries e pV q V pVr pVq V pV r R flexivit de l quivalence 3
65. e menu Edit choississez la commande Copy Placez le curseur juste l endroit o vous voulez ins rer ce bijou et copiez le cet endroit dans le menu Edit choississez la commande Paste Ensuite il vous faut effacer le th or me ou l axiome de l endroit initial ot il se terrait pour la premiere fois la fin de la liste Pour ceci cliquez sur le bouton droit de la souris sur ce th or me et appuyez sur delete dans le menu flottant Ensuite il faut v rifier syntaxiquement votre axiome ou votre th oreme pour qu il s inscrive dans la banque interne de Z EVES Attention lorsque 59 vous utilisez la commande Check sur un objet quelconque ici un axiome ou un th or me qui n a pas encore t v rifi ce moment l Z EVES enl ve la v rification de chacun des objets en dessous de cet objet Donc apr s avoir v rifi syntaxiquement votre nouvel arrivant il faut rev rifier les th or mes ou axiomes qui se sont d sactiv s durant cette op ration Si vous ajoutiez un axiome votre travail s arr te ici Votre d monstrateur contient d sormais un axiome de plus Si vous ajoutiez un th or me alors votre travail continue il faut r aliser la preuve de ce th oreme Pour parvenir ceci suivez la m thode de la section 5 2 7 pour entrer votre preuve Dans le mode graphique pour ajouter le m me nouveau th or me que celui ajout dans le mode textuel l exemple pr c dent vous auriez d ins crire theorem No
66. e mode graphique dans la plateforme Windows cliquez sur D marrer Programmes Z EVES 2 1 Z EVES GUI 2 S lectionnez dans le menu File la commande Import 3 Donnez le chemin d acc s correct pour le fichier contenant la banque d axiomes et de th or mes et appuyez sur Ouvrir Dans la pr sente recherche le fichier se nomme AlgBoolZLaTeX zed Il faudrait donc sp cifier le chemin d acc s chemin jusqu au r pertoire contenant le fichier AlgBoolZLaTeX zed ce stade ci vous devriez voir dans la fen tre Specification de votre d monstrateur tous les axiomes et th or mes avec dans les deux colonnes de droite des points d interrogation Le point d interrogation le plus gauche veut simplement signifier que cette ligne n a pas t v rifi e syntaxiquement par Z EVES Donc le d monstrateur n a pas encore accept cette ligne l Le point d interrogation droite du premier signifie simplement que l on n a pas encore prouv cette ligne l Si vous d sirez travailler avec toute la banque de th oremes il faut aller la derni re ligne d instruction le dernier th or me et appuyer sur le bouton de droite de la souris sur cette ligne ce moment l un menu flottant apparait et vous s lectionnez la commande Check up to here Ensuite vous attendez que tous les th or mes aient t v rifi s syntaxiquement Avec un Pentium II 400 MHz avec 64 Megs de m moire vive cette op ration a pris une minute
67. e preuve Z EVES consid re que la preuve est termin e et la d monstration s arr te l pour ce th or me Donc on a d montr le th or me Toutes les d monstrations peuvent se lire comme nous venons de le faire Quelquefois il se peut qu il y ait une tape que nous n avons pas expliqu e ici Pour combler cette lacune consultez la d finition de la commande que vous avez utilis e pour r aliser cette tape Normalement la signification devrait vous sauter aux yeux Vous pouvez donc maintenant lire une preuve donn e par l interface Z TEX 5 2 9 Utilisation de la banque d axiomes et de th o remes A cette tape ci vous devriez comprendre d une facon g n rale le fonc tionnement de Z EVES Maintenant voici la m thode rapide pour tre ca pable de charger notre banque d axiomes et de th or mes dans le d monstra teur pour que vous soyez capable de les utiliser De plus cette section montre comment modifier cette banque de donn es Comment acc der la banque d axiomes et de th or mes D pendant de l interface que vous choississez pour charger la banque la m thode diff rera Mode textuel En mode textuel le chargement de la banque d axiomes et de th or mes est tr s simple si vous choississez de charger la banque en entier et cela se complique un peu si vous d sirez ne charger qu une partie de la banque 54 Pour charger la banque en entier Le chargement de la banque de donn es dans son enti
68. ed 4 Attendre que la banque se charge cela risque de prendre quelque temps et vous allez voir tout au long de cette op ration des preuves d filer sous vos yeux Pour charger une partie de la banque de donn es On peut aussi raccourcir le temps d attente pour acc der aux th or mes et axiomes si on ne d sire pas avoir toute la banque pour travailler Quelquefois il est plus utile et surtout moins long de ne charger qu une partie des divers th or mes dans Z EVES Par exemple on pourrait vouloir ne charger que les trentes premiers th or mes et axiomes pour v rifier ce qu on peut prouver gr ce eux Si tel est votre d sir voil les tapes suivre pour charger seulement la 99 partie de la banque qui vous int resse 1 Ouvrez votre diteur de texte pr f r qui doit tre capable de lire des fichiers IXTEX 2 Visionnez la banque d axiomes et de th or mes et d cidez jusqu quel th or me vous d sirez charger les informations si vous choississez de prendre des th or mes de fa on parse n oubliez pas de v rifier si vous poss dez tous les th or mes et les axiomes qui sont n cessaires pour d montrer chacun des th or mes 3 Copiez les informations de ces th or mes dans le presse papier de votre systeme d exploitation 4 Ouvrez Z EVES en mode textuel dans la plateforme Windows cliquez sur D marrer Programmes Z EVES 2 1 Z EVES 5 Collez dans Z EVES les informations que
69. el de la d monstration de th oremes Pour r ussir ceci nous avons implant l int rieur de Z EVES un nouveau type le type BoolGries Ce nouveau type est en fait un ensemble que nous avons donn Z EVES en ne lui disant pas comment il tait d fini Nous lui avons donn deux constantes les constantes vrai et faux et nous lui avons sp cifi qu elles taient l ment de cet ensemble Ceci avait comme r le de cr er un type bool en Ensuite nous avons implant les op rateurs de base de Gries amp Schneider Ces op rateurs sont tous des fonctions Leur d finition de type est d finie ci dessous 2 Syntaxe de Symbole de Type de l op rateur l op rateur l op rateur equiv BoolGries x BoolGries BoolGries nonequiv xz BoolGries x BoolGries BoolGries implique gt BoolGries x BoolGries BoolGries consequence BoolGries x BoolGries BoolGries et A BoolGries x BoolGries BoolGries ou V BoolGries x BoolGries BoolGries Anon BoolGries BoolGries Nous avons donn Z EVES seulement la classe des op rateurs leur priorit et leur nombre d argument Ensuite cela nous permettait d utiliser ces op rateurs de la facon d finie par le tableau ci dessous Syntaxe de Symbole de Exemple Priorit l op rateur l op rateur d utilisation equiv p equiv q 3 nonequiv xz p nonequiv q 3 implique gt p impliq
70. entifiant mot d coration identifiant nom op V sym in d coration V sym pre d coration V V sym post d coration Ming V rimg d coration marque marque LE ix er mp posuer 8 fct in g n_in relin g n pre rel pre fct post Vbegin para opt theorem usage nom th or me par formel g n pr dicat proof commande sep sep commande end theorem axiom rule grule frule mot liste identifiant pr dicat 1 expression rel rel expression pr dicat 1 implies pr dicat 1 pr dicat_1 iff pr dicat_1 true false pr dicat 26 expression expression expression 1 expression_2 expression 2 expression_3 expression_3 expression_4 expression_4 z Locale ou_Globale nom var par eff g n Locale ou globale Local Global par eff g n z liste expression liste expression expression expression rel K lit Syntaxe ajout e celle de base par la pr sente recherche Notre but lors de cette recherche tait d implanter la logique de Gries amp Schneider dans un d monstrateur automatique de th or mes avec son syst me d axiomes et ses op rateurs Nous avons donc cr une alg bre bool enne con ue sur les axiomes et les op rateurs fournis par Gries amp Schneider qui permettait de r aliser des d monstrations de th or mes de cette logique quationnelle De plus elle favorisait un apprentissage plus natur
71. er est tr s simple mais elle est aussi tr s co teuse en temps Elle est tr s co teuse en temps car il faut que Z EVES r alise toutes les preuves des th or mes de la banque de donn es avant que la banque soit op rationnelle Le chargement de cette banque en son entier n cessite cinquante et une minutes pour un Pentium IT 400MHz avec 64 Megs de m moire vive Attention si vous d sirez r duire le d lai d attente pour le chargement de la banque de th or mes dans le but d une utilisation rapide alors remplacez toutes les occurrences du nom de fichier AlgBoolZLa TeX zed par le nom de fichier AlgBoolZLaTeX2 zed Ce fichier contient les m mes th or mes et axiomes que le fichier AlgBoolZLa TeX zed mais il ne contient aucune d monstration des divers th or mes Donc le gain de temps est tr s visible En fait ce fichier ne n cessite qu environ dix secondes pour se charger en entier Voil les tapes qu il faut suivre pour charger la banque 1 Ouvrez Z EVES en mode textuel dans la plateforme Windows cliquez sur D marrer Programmes Z EVES 2 1 Z EVES 2 S lectionnez dans le menu File la commande Read 3 Donnez le chemin d acc s correct pour le fichier contenant la banque d axiomes et de th or mes et appuyez sur Ouvrir Dans la pr sente recherche le fichier se nomme AlgBoolZLaTeX zed Il faudrait donc sp cifier le chemin d acc s chemin jusqu au r pertoire contenant le fichier AlgBoolZLaTeX z
72. er le logiciel sur leur serveur 2Ici le symbole x d signe soit le quantificateur universel V soit le quantificateur exis tentiel 3 19 Une fois que vous avez obtenu la licence et que vous tes all s cher cher votre copie de Z EVES il faut l installer Sur la plateforme Windows l installation n est pas tr s complexe Vous d compressez le fichier sp cifi du logiciel pour Windows et ensuite vous n aurez qu lancer l application concer nant l installation le fichier setup exe Ensuite vous suivez les instructions d installation Ceci permet de faire fonctionner Z EVES d une fa on partielle En effet avec cette installation il se peut que vous n avez pas acc s toutes les fonc tionnalit s du logiciel Z EVES fonctionne sur deux modes le mode textuel et le mode graphique Le mode textuel fonctionne tr s bien apr s la proc dure d installation donn e plus haut Le mode graphique utilise une interface gra phique crite en Python 1 5 2 Pour faire fonctionner cette interface vous devez avoir deux logiciels suppl mentaires disponibles gratuitement sur le web Python 1 5 2 et Tcl Tk 8 0 Python 1 5 2 est disponible l adresse URL http www pythonlabs com download C est la page officielle de la soci t qui a cr Python Tcl Tk 8 0 est disponible l adresse URL http www scriptics com software tcltk 8 0 tml C est la page des d veloppeurs de Tcl L installation de ces deux logiciels se
73. es suivant les crit res de comparaison rapidit avec d monstration complexe et simple convivialit et niveau d int r t suite 107 A 5 Adresses Internet 108 Adresse Internet Fic A 21 Adresses Internet utilis es pour l analyse des diff rents d monstrateurs automatiques de th oremes 109 http Awww irm mathematik hu berlin de ilf http Awww cs wcu edu shults FT P IPR http Awww cl cam ac uk Research HVG Isabelle http Awww ags uni sb de konrad kimba html Fic A 22 Adresses Internet utilis es pour l analyse des diff rents d monstrateurs automatiques de th or mes suite 110 Adresse Internet Kripke Larch LP Moore o ee a Fic A 23 Adresses Internet utilis es pour l analyse des diff rents d monstrateurs automatiques de th or mes suite LH Fic A 24 Adresses Internet utilis es pour l analyse des diff rents d monstrateurs automatiques de th or mes suite 112 d Otter et de FINDER Fic A 25 Adresses Internet utilis es pour l analyse des diff rents d monstrateurs automatiques de th or mes suite 113 Annexe B Annexe Axiomes implant s dans Z EVES pour la cr ation de
74. ewrite La commande rewrite fait de la r criture sur le but courant En r criture Z EVES r alise la simplification la commande simplify mentionn e plus haut et applique aussi les r gles de r criture dans l espoir de r duire le but courant Cette commande est tr s utile lorsqu on d sire utiliser plusieurs r gles de r criture rapidement Par exemple on peut souhaiter utiliser plu sieurs fois le th or me de commutativit ou d associativit de l quivalence ce moment l on peut utiliser cette commande et voir le r sultat rapidement La commande trivial rewrite est une forme tr s limit e de r criture En fait celle ci ne r alise pas de simplification et applique simplement les regles de r criture qui ne sont pas conditionnelles La commande prove by rewrite r pete la commande de r duction re write jusqu ce qu une r criture n ait pas d effet A chaque it ration les op rations suivantes sont r alis es 37 1 Le but courant subit la commande prenex cette commande est d finie dans la section 5 2 6 3 2 La commande rearrange est utilis e cette commande est d finie plus loin dans cette section 3 La commande equality substitute est utilis e voir section 5 2 6 4 4 Le but courant est modifi par la commande rewrite Reduce Cette commande est appel e suivant cette syntaxe commande reduce prove by reduce En utilisant reduce Z EVES r alise les op rations suiva
75. f use equivIdentite4 with normalization simplify rearrange use lemmel Point1 use equivCommutativitel use equivAssociativitel p q q p r p use equivIdentitel use equivldentite5 p q with disabled equivldentite2 prove by reduce Fin de l ajout de lemmes 120 theorem Modification Theo Vp q BoolGries ep q amp p q vrai proof use lemmel use lemme2 prove with normalization simplify theorem EssaiTheol Vp q BoolGries p p q q vrai proof rewrite theorem VraiTheo Vp BoolGries e vrai vrai proof prove theorem egaliteReflexivite V p BoolGries e p p proof prove Th or mes de faux theorem fauxDef2 Vp BoolGries e faux vrai vrai proof use Modification Theo p faux q 7 vrai prove theorem fauxDef3 V p BoolGries e vrai faux proof prove 21 Th or mes de la n gation theorem DistNegSurEquiv3 Vp q BoolGries e p q p q vrai proof use Modification Theo p p q q p q prove theorem DistNegSurEquiv4 Vp q BoolGriese a p q 7p q proof reduce apply equivCommutativitel to expression p q simplify rewrite Th or me de l in quivalence theorem nonequivDef2 Vp q BoolGriese 7 p q p q proof prove Th or mes de l quivalence de la n gation et de l in quivalence theorem TroisPointQuatorze Vp q BoolGriese n p q p 4q proof rewrite apply equivCommutativitel to
76. fait facilement en suivant les ins tructions du fichier readme Maintenant l interface graphique de Z EVES devrait fonctionner 5 2 3 D buter le d monstrateur Comme expliqu pr c demment Z EVES peut fonctionner en deux modes ind pendants mais ces deux modes ne peuvent coexister en m me temps Chacune des sections qui suivent sera donc s par e en deux sous sections d crivant respectivement le mode textuel et le mode graphique Mode textuel Pour d buter Z EVES en mode textuel il suffit dans la plateforme Win dows de cliquer sur D marrer Programmes Z EVES 2 1 Z EVES 20 Normalement l interface du mode textuel devrait apparaitre Mode graphique Pour lancer Z EVES en mode graphique il faut dans le syst me d ex ploitation Windows cliquer sur D marrer Programmes Z EVES 2 1 Z EVES GUI ce moment si l installation s est bien d roul e l interface graphique devrait tre visible 5 2 4 Explication des interfaces Il y a deux interfaces dans Z EVES Chacune de ces interfaces est diff rente et les outils pour faire le lien entre ces deux interfaces ne sont pas tota lement implant s dans ce d monstrateur ORA Canada continue d ailleurs d am liorer le lien entre ces interfaces Bient t les deux communiqueront sans probl mes mais la version 2 1 fait ressortir que la construction du pont n est pas termin e Mode textuel Ce mode poss de une interface qui permet
77. fini par J M Spivey voir 19 pour plus de d tails concernant cette notation EVES est un d monstrateur automatique de th o remes d velopp aussi par ORA Canada Avant de d buter La syntaxe des quantificateurs universels et existentiels utilis e dans cette recherche diff re quelque peu de la syntaxe pr conis e par Gries amp Schneider 5 Cette syntaxe est celle utilis e par Z EVES Voil la syntaxe pour ces deux quantificateurs x liste variables li es type e pr dicat Cette syntaxe diff re de celle de Gries amp Schneider surtout pour l utilisation des parenth ses En fait Z EVES n utilise pas de parenth ses pour d finir la limite de la port e des quantificateurs sa port e est d finie par le plus grand pr dicat possible apres le symbole e Le symbole e est quivalent au symbole dans la notation de Gries amp Schneider 5 2 2 Obtenir et installer Z EVES Le logiciel Z EVES Version 2 1 est disponible sur le site d ORA l adresse URL http www ora on ca z eves welcome html Ce logiciel est dis ponible au public pour une utilisation soit p dagogique soit de recherche Z EVES n a pas encore de licence pour une utilisation commerciale Il faut remplir une demande pour obtenir une licence du logiciel Cette demande doit tre post e ORA Canada et ensuite ORA Canada donnera ou non son autorisation ce moment l vous recevrez des instructions disant comment aller t l charg
78. i re possibilit pour tendre la logique propos e ici est de donner de nouveaux axiomes valides pour les op rateurs d j pr sents Si nous faisons cela nous devons faire attention de ne pas entrer en conflit avec les axiomes d j d finis pour ces op rateurs car le but est de conserver tout de m me le syst me d axiome initial pour le rendre plus puissant en l enrichissant de nouvelles connaissances Grace ceci nous venons de sp cialiser le type BoolGries aux besoins d un utilisateur particulier Donc nous venons de cr er une nouvelle th orie qui est utile pour une utilisation diff rente de celle de cette recherche du type BoolGries 71 Chapitre 6 Exemples d j test s Ce chapitre invite l utilisateur r aliser des d monstrations faciles et pratiques avec Z EVES vrai dire ce chapitre montre comment utiliser la banque d exemples cr e dans cette recherche qui peut tre r cup r e rapidement par l utilisateur Chaque fichier donn ci dessous contient un exemple d une d monstration d un th or me La r solution de ces exemples est donn e seulement pour le mode graphique de Z EVES car il permet d apprendre rapidement la d monstration de th or mes Aussi le temps de r alisation de la d monstration est tenu en compte ici car si nous de vons charger plusieurs th or mes dans Z EVES avant de pouvoir d buter la d monstration alors le mode textuel prendrait beaucoup plus de temps le mode text
79. implicationDef DistOuSurEt1 DistEtSurOul DeMorgan1 DeMorgan2 ouCommutativite ouAssociativite etAssociativite etCommutativite DistNegSurEquiv1 DistOuSurEquiv1 prove apply ouAssociativite to expression p V qV q simplify apply ouCommutativite to expression q V q simplify apply TiersExclu to expression q V q simplify with disabled RegleDOr implicationDef DistOuSurEt1 DistEtSurOul DeMorgan1 DeMorgan2 ouCommutativite ouA ssociativite etAssociativite etCommutativite DistNegSurEquiv1 DistOuSurEquiv1 prove 153 theorem TroisPointQuatreVingtOnze Vp q r BoolGries e p r q r pV q gt r proof use DefAltDeImplicationl g r use DefAltDeImplicationl p q q r use DefAltDeImplicationl p p V q q r use DeMorgan2 with disabled RegleDOr implicationDef DistOuSurEt1 DistEtSurOul DeMorgan1 DeMorgan2 ouCommutativite ouA ssociativite etAssociativite etCommutativite DistNegSurEquiv1 DistOuSurEquiv1 prove apply RegleDOr to expression p q simplify apply RegleDOr to expression p V r qV r simplify apply ouCommutativite to expression 5 q V r simplify apply ouAssociativite to expression p V rV rV q simplify use lemmel4 p r q q apply ouCommutativite to expression 7 p 7q 7pV74q Vr simplify with disabled RegleDOr implicationDef DistOuSurEt1 DistEtSurOul DeMorgan1 DeMorgan2 ouCommutativite ouAssociativite etAssociativite etCommutativite DistNegSurEquiv1 Dis
80. ining using KnownMember declarationPart knownMember internal items with the assumptions select _2 _1 select _2 _2 non declaration equiv declaration internal items to p Mn BoolGries NN land q Nin BoolGries NN implies IF non p Min BoolGries THEN q equiv non p equiv non p ELSE non p equiv q equiv non p q q Si vous d sirez connaitre exactement en quoi consiste chacun des th o r mes qui sont utilis s dans la d monstration mais qui ne proviennent pas de la logique implant e dans cette recherche vous trouverez cette information dans le Mathematical Toolkit de Z EVES 17 Il reste encore la derniere commande de la preuve ex cuter la com mande rewrite Les effets de cette commande sont d finis dans la section 5 2 6 Voil la partie qui correspond cette commande dans la preuve Which simplifies when rewriting with equivCommutativite3 applicationInDeclaredRangeFun inPowerSelf forward chaining using KnownMember declarationPart knownMember internal items with the assumptions select _2 _1 select _2 _2 53 equiv declaration fun _ type non declaration internal items to true Il n y a rien de bien nouveau traiter dans le r sultat de cette commande Nous en avons d j discut dans les autres commandes La seule diff rence est le pr dicat final le but courant Ce pr dicat est true Lorsqu on arrive avec le but courant true dans un
81. initial Commencons tout d abord par reprendre la preuve du th oreme Dis tOuSurOul Il faut pr alablement comprendre que Z EVES fonctionne de facon s quentielle Ce qui fait en sorte que nous ne pouvons utiliser dans une d monstration un th or me qui a t d fini apr s le moment o nous avons implant le th or me initial Donc nous ne pourrons utiliser l nonc de notre th oreme initial pour r aliser la preuve finale car les lemmes lemme6 et lemme ont t d finis apr s ce th or me Nous devons donc r entrer notre th or me avec un nom diff rent pour pouvoir recommencer notre preuve de ce th or me begin theorem DistOuSurOu forall p q r BoolGries p ou q ou r p ou q ou p ou r end theorem Nous sommes revenus au d but de la preuve du th or me initial Donnons notre d monstrateur des hypoth ses suppl mentaires pour ce th or me les deux nouveaux lemmes que nous venons de prouver Nous pouvons r aliser ceci gr ce aux commandes use lemme6 et use lemme7 Finalement il ne reste qu a dire 4 Z EVES de d mystifier le tout pour r aliser la preuve Essayons la commande rewrite pour effectuer cela c est la commande la mieux adapt e pour nos besoins ici rewrite Z EVES nous retourne le but courant true Z EVES a donc r ussi a 25T y aura donc deux th or mes qui auront le m me pr dicat mais avec des noms diff rents Ceci n est que pour une fin de d mo
82. ion theorem DistNegSurEgalite Vp q BoolGriese 7p qep 74q 116 theorem rule DistNegSurEquiv1 Vp q BoolGries eS p q p q theorem rule DistNegSurEquiv2 Vp q BoolGriese n p q gt p q Axiome de l in quivalence theorem rule nonequivDef Yp q BoolGries e p q pzq Axiomes de la disjonction theorem rule ouCommutativite Vp q BoolGriesep V q qV p theorem rule ouAssociativite Vp q r BoolGriesepV qV r pV qv r theorem rule ouldempotence V p BoolGries ep V p p theorem rule DistOuSurEquiv1 Vp q r BoolGriesepV q pV r pV q r theorem rule DistOuSurEquiv2 Vp q r BoolGriese p V q r pV qg pVr theorem rule TiersExclu V p BoolGries e p V p vrai Axiome de la conjonction 117 theorem rule RegleDOr Vp q BoolGriesep q p qd PV a Axiome de l implication theorem rule implicationDef Vp q BoolGries e p gt q pV q 4 Axiome de la cons quence theorem rule consequenceDef Vp q BoolGriese p q q p 118 Annexe C Annexe Th or mes test s dans Z EVES ainsi que leur preuve respective 119 Th or mes de l quivalence theorem equivIdentite5 Vp BoolGries e p vrai p proof use equivCommutativitel g vrai rewrite Ajout de lemmes theorem lemmel Vp q BoolGriesep q p q vrai proof prove theorem lemmelPoint1 Vp q BoolGriesep q gt vrai p q proof prove theorem lemme2 Vp q BoolGries p q vrai gt p q proo
83. ises Reprenons l exemple de la section 2 1 La variable p repr sente le fait je suis tudiant Faisons de m me pour les phrases je travaille et je gagne de l argent et appelons les respectivement q et r ce moment l on peut relier ces phrases pour faire des raisonnements En utilisant la syntaxe pr sent e dans la figure 2 1 on peut donner les axiomes suivants Op rateurs de quivalent en Utilisation Nom de coordination francais l op rateur Non ap N gation Et p q Conjonction V Ou pV q Disjonction gt Implique pq Implication lt Cons quence p amp q Cons quence xz In quivalent p q In quivalence Equivalent p q Equivalence Egal pq Egalit Fic 2 1 Tableau de la syntaxe de la logique propositionnelle eg r e paq gt r Le premier axiome dit que je travaille si et seulement si je gagne de l argent et le deuxi me affirme que si je suis tudiant et que je ne travaille pas alors je ne gagne pas d argent Grace cela on peut maintenant repr senter de facon simplifi e une r alit Ceci permet de repr senter les propositions plus facilement en don nant un certain degr d abstraction et permet aussi de math matiser la lo gique propositionnelle Ce rapport d crit comment cette logique a t implant e dans le logiciel Z EVES cr par ORA Canada Chapitre 3 Les diff rents d monstrateurs automatiques de th or mes 3 1
84. le ci inactive lors de l ex cution de la commande rewrite On entrerait donc comme commande with disabled RegleDOr rewrite With enabled Cette commande a la syntaxe suivante commande with enabled liste nom v nement commande Cette commande permet d activer temporairement le temps d une com mande du d monstrateur des v nements qui sont d sactiv s pour ensuite r aliser la commande sp cifi e Tenter d activer un v nement d ja activ n a pas d effet With expression La syntaxe pour la commande with expression est commande with expression expression commande Elle permet de r aliser la commande sp cifi e sur seulement toutes les occur rences de expression dans le but courant plut t que partout dans le but With predicate La syntaxe pour la commande with predicate est commande with predicate pr dicat commande Crest le th or me DistDeEtSurEt1 dans notre banque de th or me 41 Elle permet de r aliser la commande sp cifi e sur seulement toutes les occur rences de pr dicat dans le but courant plut t que partout dans le but With normalization La syntaxe pour cette commande est la suivante commande with normalization commande Avant d utiliser cette commande il faut savoir comment Z EVES repr sente les propositions dans son langage vrai dire Z EVES connait tous les op rateurs logiques sous une forme conditionnelle Par exemple pour Z EVES la pro
85. le du mode textuel et celle du mode graphique Ces formes sont presque identiques Mode textuel La syntaxe du logiciel en mode textuel est tr s proche de celle de IXTEX Syntaxe de base du Z standard Z EVES connait la syntaxe de base du Z standard mais cette syntaxe est crite en IXTEX modifi Le Z standard a une grammaire de base Plusieurs ler mes de cette grammaire ne sont pas utilis s dans cette recherche La grammaire que l on fournit ci dessous ne comprend pas les commandes destin es diriger le d monstrateur automatique de th o remes Les lex mes qui ont t omis dans cette recherche et qui font partie du Z standard sont e Les schema boxes C est l int rieur de ces boites que r sident les d finitions des sch mas en Z e Les z sections Ce sont les sections ot on peut placer les paragraphes du Z pour en faire des blocs qu on peut r f rencer e Les axiomatic boxes C est l int rieur de ces boites qu on peut donner des axiomes conform ment au Z standard qui seront pris en compte durant toute la sp cification e Les generic boxes Ce sont presque des axiomatic boxes sauf que ces boites poss dent une liste d arguments formels g n riques e Les schema definitions C est une autre mani re que celle des schema boxes pour d finir le contenu d un sch ma e Les abbreviation definitions C est une facon rapide d assigner une variable une expression e Les labelled predicates Ce sont des
86. me et s lectionnons dans le menu flottant Show proof Nous avons acc d la fen tre Proof de ce th or me Maintenant nous devons le prouver Il existe plusieurs fa ons de prouver ce th or me Nous en exposons deux ici Premi re preuve du th or me Nous proposons ici une preuve presque automatique Nous allons utiliser nos r gles de r criture et nous ne poserons pas de contraintes Z EVES pour la d monstration Ex cutons tout d abord la commande prove Ceci permet Z EVES d ap pliquer de facon r p titive la commande rewrite jusqu ce qu elle n effectue plus de transformations voir la description de la commande section 5 2 6 7 Nous obtenons le but courant suivant p BoolGries q BoolGries p equiv p ou p ou q p equiv p ou q En examinant ce but nous nous rendons compte que Z EVES n est pas capable de conclure que p ou p ou q donne p ou q Il faut donc l aider Pour 73 cela nous avons dans notre banque de th or mes un th oreme sur l associa tivit de la disjonction Utilisons le en entrant manuellement la commande dans le mini editor use ouAssociativite2 q p r qj Si tout s est bien d roul nous devrions avoir ajout dans les hypoth ses du but courant le th or me ouAssociativite2 avec les substitutions demand es Finalement nous demandons Z EVES de compl ter la preuve avec la commande prove Z EVES retourne le but courant true Voil le th
87. mme op rateur sur des pr dicats ou des sch mas e On peut cr er d autres op rateurs D savantages e Il ne poss de pas de type bool en car le Z standard n a pas la notion de bool en e Il est tr s difficile impossible dans certain cas de red finir les op ra teurs pr d finis En consid rant ces points notre choix s est port sur Z EVES car il tait plus naturel flexible et convivial que HOL98 Z EVES permet de r aliser et de visualiser les preuves plus facilement que HOL98 De plus on ne peut retracer le cheminement suivi par HOL98 pour d montrer un th or me ce qui rendait son utilisation tr s peu int ressante pour l apprentissage de la d monstration de th or mes Le logiciel cr par ORA Canada permet de suivre les tapes de la d monstration des th or mes d une fa on plus naturelle sans qu on ait l impression que Z EVES sort un lapin d un chapeau Il tait beaucoup plus int ressant pour permettre un bon apprentissage de la d monstration de th or mes de nouveaux utilisateurs Finalement Z EVES tait le choix logique pour nos besoins 1 Graphic User Interface 18 5 2 Guide d utilisation de Z EVES Version 2 1 5 2 1 Introduction Z EVES est un logiciel cr par ORA Canada C est un logiciel puissant qui conjoint la force du d monstrateur automatique de th or mes EVES avec la syntaxe du langage de sp cification Z La syntaxe utilis e du Z est celle du Z standard tel que d
88. nction nement de Z EVES et comment travailler avec celui ci 27Le premier Y signifie que le th or me est enregistr dans Z EVES et l autre Y que ce th or me a t prouv 67 5 2 11 Sp cialisation du d monstrateur L alg bre bool enne que nous pr sentons dans cette recherche est int res sante mais elle n est peut tre pas totalement adapt e aux besoins d un utilisateur particulier ce moment l la solution est d tendre la logique L augmentation de cette alg bre se r alise tr s facilement grace Z EVES et la d finition du type BoolGries que nous avons implant Tout d abord nous pouvons tendre cette logique en lui donnant de nou veaux op rateurs Cela permet d avoir de nouveaux axiomes pour d finir le comportement de cet op rateur et m me de prouver ensuite de nouveaux th or mes que nous ne pouvions pas prouver pr c demment Pour r aliser ceci nous devons tout d abord connaitre le nouvel op rateur et les axiomes le r gissant Par exemple prenons un nouvel op rateur que nous appellerons coeur et donnons lui ce symbole Q Disons que coeur a une priorit de 5 voir la figure de la section 5 2 5 et que cet op rateur est associatif commutatif et qu il peut se distribuer sur l quivalence Cet op rateur est une fonction qui prend deux arguments de type BoolGries et qui retourne un type Bool Gries Nous devons commencer par d clarer ce nouvel op rateur en suivant la synt
89. ngt Vp q BoolGries ep q p p proof use DefAltDeImplication2 p q q p use TroisPointSoizante q q p r q apply etCommutativite to expression q p simplify use lemme19 use equivIdentitel p p q with disabled RegleDOr etCommutativite etAssociativite equivAssociativitel equivCommutativitel equivCommutativite3 prove 146 theorem TroisPointQuatreVingtUn Vp q BoolGries e p V p gt q vrai proof apply implicationDef simplify use DistOuSurEquiv2 q p V q r q apply ouCommutativite to expression p V p V q simplify apply ouCommutativite to expression p V q simplify apply ouAssociativite to expression q V p V p simplify apply ouldempotence simplify with disabled ouAssociativite ouCommutativite prove theorem TroisPointQuatreVingtDeux Vp q BoolGriesep V q p q gt p proof apply implicationDef simplify use DistOuSurEquiv2 g q V p r p apply ouCommutativite to expression q V p simplify use lemme14 apply ouldempotence simplify with disabled ouA ssociativite ouCommutativite prove 147 theorem TroisPointQuatreVingt Trois Vp q BoolGries ep V q gt p q pzq proof apply implicationDef to expression p V q p q simplify use DistOuSurEt1 p p V q q p r q apply ouAssociativite to expression p V q V p simplify apply ouCommutativite to expression q V p simplify use lemme14 apply ouAssociativite to expression p V q V q simplify apply ouldempotence to
90. nstration seulement Apr s vous n avez qu transcrire les th oremes dans le bon ordre et vous n aurez pas d finir deux fois le m me th or me avec des noms diff rents Z EVES ne tentera pas de d montrer le second th or me l aide de l nonc du premier car le premier th or me a t implant sans usage donc Z EVES ne peut l utiliser automatiquement 65 d montrer le th or me Maintenant ce th or me est accessible pour une uti lisation future Cette d monstration s est effectu e dans le mode textuel Mode graphique Dans le mode graphique la preuve est th oriquement la m me que celle dans le mode textuel Donc vous n aurez pas refaire un cheminement com plexe pour arriver la d monstration Commengez tout d abord par ouvrir Z EVES en mode graphique et chargez la banque de th or mes jusqu au th or me DistOuSurOu1 pour la r alisation de cette tape voir la section 5 2 9 Pour cette d monstration vous vous tes pargn s l criture de ces th o r mes dans le mode graphique mais cela est uniquement car vous avez d j r alis la m me chose dans le mode textuel L criture d un th or me dans le mode graphique ne devrait pas vous poser de difficult s Cliquez sur le bouton droit de la souris sur le th or me lemme6 et s lec tionnez la commande Show proof dans le menu flottant qui apparait Ceci vous a permis d acc der la fen tre Proof pour le th or me lemme6 Ce lemme se
91. ntes il effectue une simplification simplify une r criture rewrite et il remplace toutes les r f rences des sch mas ou des instances g n riques des op rateurs par leur d finition respective et ensuite le r sultat est r duit une autre fois La commande prove by reduce r p te la commande de r duction reduce jusqu ce qu une r duction n ait pas d effet A chaque it ration les op rations suivantes sont r alis es 1 Le but courant subit la commande prenex cette commande est d finie dans la section 5 2 6 3 2 La commande rearrange est utilis e cette commande est d finie plus loin dans cette section 3 La commande equality substitute est utilis e voir section 5 2 6 4 4 Le but courant est modifi par la commande reduce Rearrange Une quatri me commande pourrait se rajouter la mani re automatique d utiliser les th or mes et les d finitions mais celle ci ne tente pas de r duire le but courant Sa seule fonction est de r arranger les hy poth ses pour que les hypoth ses apparaissent dans un ordre plus simple pour Z EVES ce qui permet d augmenter l efficacit et la rapidit des com mandes de r duction Sa syntaxe est celle ci commande rearrange 38 5 2 6 3 Les quantificateurs Les quantificateurs internes de Z EVES ont deux commandes sp ciales qui sont utiles pour leur manipulation dans le d monstrateur Instantiate La syntaxe suivante est d finie pour cette commande
92. omatique de th or mes Nous pr conisons un d monstrateur crit dans un langage d actualit et simple d apprentissage e La convivialit du d monstrateur automatique de th or mes Nous d sirons un d monstrateur ayant une convivialit acceptable pour tre capable de r aliser des d monstrations devant public e Le type d interaction du logiciel Une interaction flexible est la bienve nue e La rapidit du d monstrateur lors de la r alisation d un probl me com plexe et d un probl me simple Il est difficile d obtenir ce renseignement et c est le crit re le moins important pour cette pr sente recherche Tant que le logiciel peut r aliser des preuves dans un temps raisonnable il est convenable ce moment l Ces crit res ont t d termin s avant d entreprendre l analyse des diff rents d monstrateurs automatiques de th or mes 3 2 Les d monstrateurs v rifi s La pr sente recherche est bas e sur la liste intitul e overview of systems implementing mathematics in the computer de Freek Wiedijk Cette liste contient deux cent dix neuf outils diff rents Parmis ces outils quatre vingt ont t v rifi s dans cette recherche Nous nous limitions dans la liste aux cat gories d outils nomm es theorem prover first order prover et tactic pro ver 2Cette liste est disponible sur internet l adresse http www cs kun nl freek digimath index html 21 Les cat gories qui n ont pas t
93. onstrateur de th or mes semi automatique il faut aider HOL trouver les preuves La puissance maximale de ce d monstrateur automatique de th o r mes est trop lev e pour les besoins de la cause Il n a pas encore t test sur les plateformes Windows 95 98 4 3 HOL Light HOL Light 11 est dans la m me lign e que HOL98 ils font partie de la m me famille de d monstrateurs automatiques de th or mes De m me que son pr d cesseur HOL Light est capable de d montrer des th or mes de la logique classique Il est programm en CAML Light Avantages de HOL Light 1 Il donne plusieurs outils pour la r solution automatique et il offre des th or mes math matiques d j prouv s contrairement ses pr d cesseurs 13 Son manuel d instruction est concis et clair il contient une centaine de pages 12 3 Ce d monstrateur automatique de th or mes est facilement adaptable 4 5 6 Il est gratuit Il peut manipuler la th orie des ensembles Il est surtout utilis en math matique c est son point fort D savantages de HOL Light 1 2 Il fonctionne avec un mode d interaction de type dialogue Ce logiciel ne fonctionne que sur une plateforme Unix 4 4 Otter Le d monstrateur automatique de th or mes Otter 13 est un logiciel crit en C et ayant un syst me de d monstration bas sur la r solution Avantages de Otter Ct 1 Il est gratuit 2 Il e
94. onstructive Solaris ordre classique ordre classique L mne constructive Z EVES Unix Common Logique classique Fic A 5 Tableau sur les diff rences entre les d monstrateurs automatiques de th or mes suivant les criteres de comparaison plateforme langage de base et puissance maximale suite 89 A 2 Qualit de la bibliographie et type d in teraction 90 qualit de la Type bibliographie d interaction 3TaP Tr s bonne livre d instruction de 190 pages contenant Script le livre de l utilisateur la description de l implantation de 3TaP et un document relatant l historique de 3TaP ACL2 Excellente environ 900 pages Analytica Mauvaise presque inexistante Mauvaise le manuel d instruction Fic A 6 Tableau sur les diff rences entre les d monstrateurs automatiques de th oremes suivant les criteres de comparaison qualit de la bibliographie et type d interaction 91 qualit de la Type bibliographie d interaction FINDER bonne manuel d instruction de 77 pages il HOL98 Excellente plus de 800 pages de bibliographie officielle HOL Light Tr s bonne environ une centaine de pages pour le livre d instruction Tr s bonne livre Isabelle Isar Fic A 7 Tableau sur les diff rences entre les d monstrateurs automatiques de th oremes suivant les criteres de comparaison qualit de la bibliographie et type d interaction suite 92 qualit de la Type bibliographie d interac
95. or me soit d une mani re temporaire soit d une mani re permanente Pour ajouter un axiome ou un th or me d une mani re permanente cela est facile Il s agit simplement d diter le fichier contenant l alg bre bool enne fournie dans cette pr sente recherche ce fichier s appelle AlgBoolZ LaTeX zed dans votre diteur de texte favori qui supporte TEX Ensuite vous vous d placez l endroit ot vous souhaitez ins rer le nouveau th or me ou axiome et vous crivez tout simplement cet endroit le nouveau th or me ou axiome d sir Attention il faut respecter la syntaxe d finie dans la sec tion 5 2 5 pour que Z EVES accepte votre entr e De plus il ne faut pas oublier que si vous entrez un th or me alors vous devez connaitre les com mandes n cessaires la r alisation de sa preuve vous ne pourrez la v rifier dans votre diteur de texte vous devrez charger le fichier dans Z EVES pour savoir si ces commandes sont exactes Ensuite vous enregistrez le tout et le tour est jou Votre banque est maintenant enrichie d un axiome ou d un th oreme de plus de facon permanente Pour v rifier si tout a bien fonctionn vous pouvez charger votre nouvelle banque dans Z EVES Si vous souhaitez ajouter un th or me d une mani re temporaire ceci devra se r aliser dans Z EVES La facon d ajouter un axiome ou un th or me est diff rente selon le mode utilis Mode textuel Pour le mode textuel apr s avoir charg v
96. otre banque de th oremes initiale vous inscrivez tout simplement la ligne de commande le nouveau th or me ou axiome que vous d sirez implanter Celui ci devra 58 respecter la syntaxe du Z IATEX telle que d finie dans la section 5 2 5 Il faut aussi r aliser la preuve ensuite si vous avez entr un nouveau th or me Par exemple vous auriez pu vouloir ajouter ce nouveau th oreme Vp q r BoolGriesep qVrz pq V p r A ce moment l vous auriez dt crire begin theorem NouveauTheoreme forall p q r BoolGries p implique q ou r p implique q ou p implique r proof use DefAltDeImplicationilq q ou r use DefAltDeImplicationi use DefAltDeImplicationl q r use DistOuSurOu1 p non pl with disabled implicationDef DeMorgani DeMorgan2 ouAssociativite ouCommutativite prove end theorem Mode graphique Pour ajouter un axiome ou un th or me dans le mode graphique commencez tout d abord par charger votre banque de donn es dans l interface graphique de Z EVES Ensuite s lectionnez la fen tre du mini editor et entrez votre axiome ou votre th or me en suivant la syntaxe montr e la section 5 2 7 Ne vous pr occupez pas maintenant de la preuve du th or me Tout d abord v rifiez o vous souhaitez implanter ce nouveau th or me ou axiome dans votre liste Ensuite copiez votre th or me ou axiome dans le presse papier de Z EVES s lectionnez votre nouvel arrivant et dans l
97. p r q apply ouCommutativite to expression r V p simplify apply ouCommutativite to expression r V q simplify prove apply ouCommutativite to expression r V p V q simplify apply equivCommutativitel to expression p V qY r DV q r r P 49 9V r simplify apply equivCommutativitel to expression r p q qV r simplify apply equivAssociativitel to expressionp q qVr simplify apply equivCommutativitel to expression p q q V r simplify use equivAssociativitel p q q V r q use lemmel5 p p V g r g q qgVrr pzrl prove Th or mes de l implication 142 theorem DefAltDelmplication1 Vp q BoolGriese p gt q 7pV q proof apply implicationDef simplify apply ouCommutativite to expression p V q simplify use TroisPointQuaranteDeux4lp q q p apply ouCommutativite to expression q V p simplify prove theorem DefAltDelmplication2 Vp q BoolGries e p gt q p qzp proof use RegleDOr2 use implicationDef apply equivCommutativitel to expression p V q q simplify prove theorem Contrapositivite Vp q BoolGries e p gt q 7q gt p proof use DefAltDeImplicationl use TroisPointQuaranteDeux2 p p apply ouCommutativite to expression 5 p V q simplify use implicationDef p q q p prove theorem rule TroisPointSoixanteQuinze Vp q r BoolGries ep gt q r pAq pAr proof use DefAltDeImplication2 q q r use TroisPointSoixante prove 143 theorem Di
98. plify apply DistOuSurEquiv2 to expression p V q p V q simplify use lemme14 use lemmelA q r with disabled equivAssociativitel equivCommutativitel equivCommutativite3 ouAssociativite ouCommutativite rewrite use lemmel4 q q V r use equivAssociativitel p p V r pV qV r q p r pv q use equivCommutativitellp p V r2 pV qV r q pzspv r use equivldentitel p p V r use equivCommutativitel p p V q V r q qV r with disabled equivAssociativitel equivCommutativitel equivCommutativite3 ouAssociativite ouCommutativite DistOuSurEquiv1 DistOuSurEquiv2 prove rewrite theorem DistEtSurOu2 Vp q r BoolGries e p q V pA r 2 p qV r proof use DistEtSurOul prove 135 theorem rule DeMorgan1 Vp q BoolGriese p q 7pV7q proof prove use TroisPointQuaranteDeux2 p p q q rewrite apply DoubleNegation to expression q simplify apply ouCommutativite to expression p V q simplify use TroisPointQuaranteDeuxA p q q p apply equivCommutativitel to expression q V p p simplify prove theorem rule DeMorgan2 Vp q BoolGries eS pV q 7pA7q proof apply RegleDOr to expression p q simplify use TroisPointQuaranteDeux2 apply equivCommutativitel to expression p V 5 q p simplify apply ouCommutativite to expression p V q simplify use TroisPointQuaranteDeux2 p q q p prove 136 theorem TroisPointCinquanteNeufl Vp q BoolGriesep q pA7q 7p proof prove
99. position p q est repr sent e l interne par l expression if p then q else false Par d faut la forme conditionnelle est d sactiv e dans Z EVES car cette forme a tendance r p ter inutilement des donn es ce qui rend les expres sions longues Donc nous ne voyons que les symboles des op rateurs et nous n utilisons pas leur d finition interne En utilisant cette commande Z EVES normalise les expressions pour les mettre dans son langage interne r alise une r duction de la forme condition nelle sous une forme plus int ressante et ensuite il ex cute la commande d sir e Ceci a pour effet d augmenter la puissance de Z EVES mais rend les expressions beaucoup plus longues et voire m me incompr hensibles Cette commande est surtout utile et int ressante lorsque le but courant est une disjonction 5 2 6 6 Retour en arri re Il y a deux commandes qui permettent de revenir en arri re lors d une d monstration Back xxx La syntaxe pour cette commande est commande back nombre Cette commande permet de revenir en arri re de nombre tapes dans la preuve Si aucun nombre n est indiqu alors Z EVES revient en arri re d une tape Z EVES perd le cheminement r alis pour ces nombre tapes lors de l ex cution de cette commande On doit donc les r aliser de nouveau si on d sire revenir la situation o on a ex cut cette commande 42 Retry xxx Cette commande est d finie comme suit commande
100. prises en compte dans cette recherche sont logic education computer algebra proof checker specification environment information repre sentation et authoring Pour mieux visualiser les diff rences entre les diff rents d monstrateurs automatiques de th or mes les donn es ont t regroup es sous forme de tableaux les tableaux A 1 A 25 dans l annexe A L annexe A 1 fournit le tableau contenant les informations sur les diff rences entre les d monstrateurs sur les crit res des plateformes que sup portent le d monstrateur automatique de th or mes du langage dans lequel est crit le d monstrateur et de la puissance maximale de cet outil L annexe A 2 montre les diff rences entre les d monstrateurs pour la qua lit de la bibliographie et le type d interaction L annexe A 3 pr sente le co t de l implantation pour chacun des d monstrateurs automatiques de th or mes L annexe A 4 donne les diff rences entre les d monstrateurs automatiques de th or mes pour les crit res suivants la rapidit pour les d monstrations simples et complexes la convivialit et le niveau d int r t soulev par chacun d eux pour cette recherche Finalement l annexe A 5 fournit l adresse Internet utilis e pour retrouver les informations concernant chacun de ces d monstrateurs 4Seule l adresse URL est donn e 10 Chapitre 4 Les d monstrateurs automatiques de th or mes qui ont t approfondis
101. propositionnelle Lisp ordre ATMS Moore prover Macintosh Lisp Lisp ML constructive a constructive Unix Lisp premier ordre Prolog ordre classique Fic A 3 Tableau sur les diff rences entre les d monstrateurs automatiques de th or mes suivant les criteres de comparaison plateforme langage de base et puissance maximale suite 87 plateforme Langage Puissance de base maximale DOS Windows ordre classique constructive d autres plateformes CAML constructive constructive Prolog Lisp et constructive ML ou Prolog premier ordre i Logique classique que de prem Logique classique A i i i PROTEIN i Eclipse Logique de premier Prolog ordre classique i N Logique de premier ordre i Satchmo i Prolog Logique de premier ordre classique Saturate i Prolog Logique de premier i ordre classique Fic A 4 Tableau sur les diff rences entre les d monstrateurs automatiques de th or mes suivant les criteres de comparaison plateforme langage de base et puissance maximale suite Zeta Lisp Log ier ordre classique 88 plateforme Langage Puissance de base maximale SCOTT combinaison Unix C d Otter et de FINDER SEM Unix N A Logique de premier ordre SETHEO Unix N A Logique de premier ordre classique A Logique de premier ordre classique Windows 95 98 NT Lisp ordre classique Windows 95 98 NT ordre classique ordre classique ordre classique Macintosh TPS Unix Common WEE GEN mne Lisp c
102. q non p equiv q Pour entrer cet axiome dans le mode graphique il faut tout d abord s lectionner la fen tre Specification et il faut atteindre la fen tre du mini editor Ensuite vous crivez l axiome dans cet diteur de texte et vous allez s lectionner dans le menu File Done Finalement vous cliquez sur le bouton de droite de la souris sur l axiome en question pour aller s lectionner dans le menu flottant l option Check Ceci vous dira si Z EVES accepte l axiome Comment entrer un th or me Pour donner un th or me Z EVES dans le mode graphique il faut tout d abord entrer le th or me comme si on entrait un axiome Ensuite on fait v rifier syntaxiquement le th or me par le d monstrateur qui accepte le th or me s il correspond la grammaire de Z EVES La derni re tape consiste pour diff rencier un th or me d un axiome r aliser la preuve de ce th or me pour qu il devienne effectivement un th or me pour Z EVES Pour donner une preuve dans le mode graphique il faut cliquer sur le bouton droit de la souris sur votre th or me et vous s lectionnez l option Show proof Ceci vous fera acc der la fenetre Proof Dans cet environnement il faut entrer les commandes une une pour diriger le d monstrateur automatique de th or mes de la m me mani re que celle pr sent e dans la section 5 2 6 Une fois que la preuve est compl t e vous revenez la fen tre Specifica tion et cela vous perme
103. q ou p 12 rewrite Nous utilisons la commande rewrite comme derni re commande simple ment parce que cette commande r alise un raisonnement sur les pr dicats conditionnels plus puissant que celui de la commande simplify En effet si nous utilisons la commande simplify alors cela ne r duit pas le but true mais au contraire le transforme en un pr dicat d sagr able d montrer Deuxi me exemple ExTheoMoyenLogProp tex Essayons de d montrer un th or me plus difficile que le pr c dent le th or me d montrer du fichier Er TheoMoyenLogProp tex C est le th or me suivant que nous voulons donc d montrer Vp q r BoolGriesep q Arz p q pr Ce th or me se d montre facilement l aide de notre banque de th or mes Tout d abord chargeons le fichier ExTheoMoyenLogProp tex dans le mode graphique Ensuite acc dons la fen tre Proof du th or me TheoremeA De montrer Pour r aliser la preuve de ce th or me il suffit que nous entrions les commandes suivantes 1 use DefAltDeImplication1 q q et r use DefAltDelmplication1 use DefAltDelmplication1 q r use DistOuSurEt1 p non p with disabled implicationDef ouAssociativite ouCommutativite et Commutativite etAssociativite DeMorgan1 DeMorgan2 DistOuSu rEt1 DistEtSurOul RegleDOr prove Ce qui revient effectuer la preuve suivante 75 Vp q r BoolGriesep q rz p q p r DefAltDelImplicationl 3 72 avec q 2 q r
104. ques de th or mes suivant les crit res de comparaison qua lit de la bibliographie et type d interaction suite Tableau sur les diff rences entre les d monstrateurs automa tiques de th or mes suivant les criteres de comparaison qua lit de la bibliographie et type d interaction suite A 9 Tableau sur les diff rences entre les d monstrateurs automa tiques de th or mes suivant les crit res de comparaison qua lit de la bibliographie et type d interaction suite A 10 Tableau sur les diff rences entre les d monstrateurs automa tiques de th or mes suivant les crit res de comparaison qua lit de la bibliographie et type d interaction suite A 11 Tableau sur les diff rences entre les d monstrateurs automa tiques de th or mes suivant le crit re de comparaison co t de limplantation oda aute A GAS DINAN da qu ee BN bus A 12 Tableau sur les diff rences entre les d monstrateurs automa tiques de th or mes suivant le crit re de comparaison co t de l implantation suite ein os mu aA oS aeree a A 13 Tableau sur les diff rences entre les d monstrateurs automa tiques de th or mes suivant le crit re de comparaison co t de l implantation suite us wa RUE et ARE de s A 14 Tableau sur les diff rences entre les d monstrateurs automa tiques de th or mes suivant le crit re de comparaison co t de l implantation Sulle
105. r use DefAltDeImplication1 with disabled implicationDef prove apply DistNegSurEquiv2 to expression q p V q simplify use DistOuSurEquiv2 p 2 p q q r p V q use DistOuSurEquiv2 p r q 5 p V 5 qr pV pV q use lemme18 with disabled DistNegSurEquivl DistNegSurEquiv2 equivA ssociativite2 ouAssociativite ouCommutativite equivAssociativitel equivCommutativitel equivCommvutativite3 DistOuSurEquiv2 DistOuSurEquiv1 equivIdentite2 prove theorem Transfert Vp q r BoolGries e p q r p q r proof use DefAltDeImplication2 p p q q r use DefAltDeImplication2 p q q r use DefAltDeImplication2 q q r q with disabled RegleDOr implicationDef prove Ajout de lemme 145 theorem lemme19 Vp q BoolGriesep p q p q proof apply etCommutativite to expression p p q simplify apply etCommutativite to expression p q simplify apply etAssociativite to expression q p p simplify with disabled RegleDOr etCommutativite etAssociativite prove Fin de l ajout de lemme theorem TroisPointSoixanteDixNeuf Vp q BoolGries e p p q p q proof use DefAltDeImplication2 with disabled RegleDOr implicationDef prove apply equivCommwutativitel to expression p p q simplify use TroisPointSoirzanteEtUn q p q use lemme19 with disabled RegleDOr etCommutativite etAssociativite prove theorem TroisPointQuatreVi
106. r duire Les autres sous buts sont accessibles seulement avec la commande next Next La commande next est d finie par la syntaxe suivante commande next Cette commande ne fonctionne qu en conjonction avec la commande cases Elle permet de changer de sous but apr s avoir r alis un cases Il n est pas n cessaire d avoir termin la preuve du sous but courant pour changer de sous but 3l Split La syntaxe de la commande split est commande split pr dicat La commande split P o P est un pr dicat permet de transformer un but G en un nouveau but Le but G devient if P then G else G Attention le pr dicat P doit respecter le type du but G Autrement dit on ne peut faire appara tre de nouvelles variables dans P Conjunctive Cette commande est d finie par la syntaxe suivante commande conjunctive Cette commande ne fait qu effectuer les transformations suivantes sur le but courant 1 Toutes les implications les quivalences et les pr dicats conditionnels sont remplac s d une fa on quivalente par les op rateurs de conjonc tion et de disjonction Attention ces transformations ne sont effectu es que sur les op rateurs cit s plus haut faisant partie de la grammaire initiale de Z EVES et non sur les op rateurs que l on a implant s par la suite 2 La port e de l op rateur de n gation de Z EVES est minimis e Par exemple VX e P devient apr s transformation 4X e P 3 Z EVES effect
107. r la d monstration de th or mes de la logique proposi tionnelle Cette logique a t implant e dans Z EVES et son utilisation est aussi expliqu e dans le manuel d utilisation de Z EVES Tout ceci dans le but de favoriser un apprentissage humain de la d monstration de th or mes l aide d un d monstrateur automatique de th or mes Chapitre 1 Introduction 1 1 Motivation L informatique prend de plus en plus de place dans nos vies Un ordina teur fonctionne grace aux diff rentes logiques implant es en son sein Une des logiques primordiales pour le bon fonctionnement d un ordinateur est la logique dite classique Cette logique a pour but de recr er le principe de raisonnement des math matiques o l ambiguit et l impr cision ne sont pas une bonne option 7 La logique classique en subdivis e en plusieurs parties et celle qui est la plus l mentaire est la logique propositionelle Pour concevoir de bons logiciels ceux ci doivent pouvoir se d crire presque toujours par la logique classique Donc pour am liorer la recherche de bogues dans les logiciels de m me qu am liorer le temps de production des logiciels nous devons d velopper des outils pour v rifier ceux ci Un des meilleurs ou tils pour cette v rification est un d monstrateur automatique de th oremes Un d monstrateur automatique de th oremes est un logiciel qui peut traiter une logique quelconque dans le cadre de cette recherche nous ne traite
108. ram tres formels g n riques alors on doit indiquer les param tres effectifs g n riques que l on d sire utiliser dans le th or me Prenons comme exemple le th or me inCupP un th or me d j pr sent dans Z EVES son d marrage Celui ci poss de un param tre formel g n rique appel X Si on d sire ajouter ce th or me aux hypoth ses de notre but courant alors il faut sp cifier l ensemble X Supposons que nous restons dans la logique implant e dans Z EVES par cette pr sente recherche ce moment l nous pouvons utiliser comme param tre effectif g n rique l en semble BoolGries d fini plus haut On appellerait donc ce th or me grace la commande suivante use inCup BoolGries Pour chaque variable d un th or me on peut renommer ou substituer On renomme en utilisant la syntaxe suivante expression voulue variable libre du th ore me La substitution se r alise suivant cette syntaxe variable libre du th or me expression voulue On ne peut utiliser un th or me avec la commande use que si toutes ses variables apr s avoir renomm et effectu les substitutions exig es dans le 13Ce th or me est la d finition de l union dans Z EVES 35 th or me sont des noms de variables que l on retrouve dans le but courant Par exemple si on a comme but courant Vp q BoolGries p V p V q p V q et qu on d sire utiliser le th or me de l associativit de la disjon
109. re des d monstrations de th or mes pour cette logique 17 EVES a t cr par ORA Canada lors du projet TR 97 5505 04g d but en janvier 1996 15 Premi re partie Quatre vingt diff rents d monstrateurs automatiques de th or mes Chapitre 2 La logique propositionnelle 2 1 Introduction la logique propositionnelle Il y a plusieurs logiques diff rentes Une de celles ci est la logique clas sique Elle a t cr e pour r diger les principes de raisonnement des math matiques o l ambiguit et l impr cision sont une mauvaise chose 7 Le but de cette logique est de cr er un monde id al un mod le math matique Cette logique est compos e d autres logiques dont l une est la logique propo sitionnelle La logique pr sent e ici est bas e sur la logique quationnelle de Gries amp Schneider 5 La logique propositionnelle est une logique partisane de la doctrine disant que tout est blanc ou tout est noir La logique propositionnelle permet de repr senter d une fagon simplifi e et non ambig e des r alit s surtout des affirmations Prenons comme exemple la phrase suivante je suis tudiant Cette phrase peut tre repr sent e par une variable bool enne qui peut tre soit vraie soit fausse Appelons cette variable p La variable p ne pourra tre vraie que si en ce moment je suis r ellement un tudiant Autrement p est fausse Cette logique permet aussi de faire des arr
110. ridge Computer Laboratory avril 2000 8l 13 Mathematics and Computer Science Division Otter An Automa 14 15 16 17 18 19 20 21 ted Deduction System Argonne National Laboratory 2001 http www unix mcs anl gov AR otter William W McCune Otter 3 0 Reference Manual and Guide Argonne National Laboratory 9700 South Cass Avenue janvier 1994 Irwin Meisels Software Manual for Windows Z EVES Version 2 1 ORA Canada One Nicholas Street Suite 1208 Ottawa Ontario KIN 7B7 juillet 2000 Irwin Meisels and Mark Saaltink The Z EVES Reference Manual for Version 1 5 ORA Canada One Nicholas Street Suite 1208 Ottawa Ontario KIN 7B7 septembre 1997 Mark Saaltink The Z EVES 2 0 Mathematical Toolkit ORA Canada One Nicholas Street Suite 1208 Ottawa Ontario KIN 7B7 octobre 1999 Mark Saaltink The Z EVES 2 0 User s Guide ORA Canada One Nicholas Street Suite 1208 Ottawa Ontario KIN 7B7 octobre 1999 J M Spivey The Z Notation A Reference Manual Second Edition Prentice Hall 1992 Daryl Stewart Automated Reasoning Group HOL page Universit de Cambridge 2000 http www cl cam ac uk Research HVG HOL Freek Wiedijk Overview of systems implementing mathematics in the computer Liste disponible sur internet l adresse http www cs kun nl freek digimath index html 2001 82 Troisi me partie Annexes 83 Annexe A Annexe Diff
111. rmettre Z EVES de couvrir tous les cas possibles Par exemple si nous avions d fini les axiomes 3 2 et 3 3 sans nous soucier de ce d tail nous aurions obtenu ces deux axiomes r Vp q r BoolGriesep z qz r pz q Vp q BoolGriesep q q p et ceux ci auraient t insuffisants pour d montrer certains th or mes Voici un exemple d un tel th or me 16En tant que tel la grammaire de Z EVES sur les pr dicats est moins restreinte que celle pr sent e ici mais nous vous pr sentons seulement la partie pertinente pour cette recherche Les mots en italiques dans la grammaire repr sente les modifications de la grammaire r alis es pour une meilleure compr hension de la formation des pr dicats dans cette recherche Cette num rotation des th or mes est la m me que celle utilis e dans les notes de cours du cours Logique et Structures Discr tes 4 44 pr dicat pr dicat 1 rel expression expression 1 expression 2 expression 3 expression 4 op rateur infixe op rateur pr fize d claration d cl basique liste noms d clar s nom d cl type forall d claration pr dicat 1 pr dicat_1 expression rel rel expression pr dicat Mn expression 1 expression 2 expression 2 op rateur infixe expression 2 op rateur pr fire expression 2 expression 3 expression 4 Locale ou Globale nom var par eff_g n equiv nonequiv Vet Vou tmplique consequen
112. roDeEt2 Vp BoolGries e faux p faux proof with disabled fauxDef rewrite theorem ZeroDeEt3 V p BoolGries e faux p faux proof with disabled fauxDef rewrite theorem ZeroDeEt4 V p BoolGries e faux faux p proof with disabled fauxDef rewrite Ajout de lemmes theorem lemmel11 Vp q r BoolGries e p q r p p q r proof with disabled RegleDOr rewrite theorem lemme12 Vp q r BoolGries ep p q r p q pAr proof with disabled RegleDOr etIdempotence rewrite apply etCommutativite to expression q p r simplify with disabled RegleDOr rewrite 131 Fin de l ajout de lemmes theorem DistEtSurEt1 Vp q r BoolGries ep qN r p q p r proof use lemmell use lemme12 with disabled RegleDOr rewrite theorem DistEtSurEt2 Vp q r BoolGries ep q p r p q r proof use DistEtSurEt1 with disabled RegleDOr etCommutativite etAssociativite rewrite theorem rule Contradiction Vp BoolGries e p p faux proof with disabled fauxDef rewrite apply equivCommutativitel to expression p p simplify use TroisPointDizHuitl rewrite theorem Absorptionl Vp q BoolGries e p pV q p proof rewrite apply DistOuSurEquiv2 to expression p V q p V q simplify use ouAssociativite2 q p r q rewrite 132 theorem Absorption2 Vp q BoolGries ep V pA q p proof rewrite apply DistOuSurEquiv2 to expression p V q p V q simplify use
113. rons que de la logique classique de premier ordre Les d monstrateurs automatiques de th or mes qui traitent de la logique classique de premier ordre ont d autres utilit s Parmi celles ci on retrouve l aide la recherche en math matiques et en informatique et l aide l ap prentissage de la logique pour des humains Cette recherche vise surtout l apprentissage de la d monstration de th or mes l aide d un d monstra teur automatique de th or mes 1 2 Pr sentation du projet Ce rapport vise tudier et comprendre les d monstrateurs automa tiques de th or mes en g n ral avec un grand accent sur les d monstrateurs qui traitent de la logique classique de premier ordre Les d monstrateurs fonctionnant avec une autre logique ne seront que mentionn s Quelques uns de ceux pr sent s seront approfondis et un d entre eux sera pr sent en pro fondeur Z EVES Version 2 1 C est le d monstrateur automatique de th o r mes que nous pr coniserons dans ce rapport conform ment aux crit res de comparaison Celui ci sera pr sent par un guide d utilisation qui permettra de mieux le comprendre et de l utiliser dans le cadre d un apprentissage pour la d monstration rigoureuse de th or mes Cette recherche se base sur la logique quationnelle de Gries amp Schneider 5 Notre but est de r ussir implanter cette logique dans le d monstrateur automatique de th or mes Z EVES Version 2 1 pour permettre de fai
114. s implanter nous n avons donn que leur d finition selon les op rateurs que Z EVES connaissait d j Voil la syntaxe ajout e pour notre th orie des ensembles TT syndef surensemble inrel surensemble syndef surensembleP inrel surensembleP begin gendef X _ surensemble _ _ surensembleP _ power X rel power X NN complement power X fun power X where Label rule surensembleDef forall S T power X T surensemble S iff S Nsubseteq T NN Label rule surensemblePropreDef forall S T power X T surensembleP S Miff S subset T NN Label rule complementDef forall S power X v X v Min Ncomplement S iff v in X land v notin S end gendef Ceci statue simplement que le surensemble est une relation infix e entre deux arguments de type P X et que cette relation poss de la d finition suivante VS T PX eT Ds s CT De plus cela affirme que l op rateur surensemble propre est une relation infix e entre deux arguments de type P X Voila sa d finition YS POpXwTescscuo Les derni res lignes donnent la d finition de l op rateur compl ment qui est une fonction de IP X dans IP X Sa d finition est celle ci VS PX u XeveEenSSvEX Aves Les d finitions que nous donnons des trois nouveaux op rateurs sont donn es en fonction des op rateurs de base de Z EVES Tout ceci a permis de cr er une banque d exemples de th or mes que nous pouvons utiliser dans l
115. s bonne livre Dialogue d instruction volumineux Fic A 10 Tableau sur les diff rences entre les d monstrateurs automatiques de th oremes suivant les criteres de comparaison qualit de la bibliographie et type d interaction suite 95 A 3 Cott de l implantation 96 Co t de l implantation Un compilateur Prolog ACL2 Un compilateur Common Lisp Analytica Un logiciel Math matica environ 895 pour une license de professeur 0 Un compilateur Prolog 3 8 au minimum Les logiciels Objective Calm gratuit et Calmp4 version 3 01 gratuit Fic A 11 Tableau sur les diff rences entre les d monstrateurs automatiques de th or mes suivant le crit re de comparaison co t de l implantation 97 Co t de l implantation FINDER Un compilateur C Frapps Un compilateur Common Lisp FT Un compilateur C GANDALF Soit rien 0 si seulement l ex cutable HOL98 Fic A 12 Tableau sur les diff rences entre les d monstrateurs automa tiques de th or mes suivant le crit re de comparaison co t de l implantation suite 98 Co t de l implantation disponible 0 LeanTaP Un compilateur Le logiciel Standard ML gratuit Soit rien gratuit si on utilise la version sur le web ou un compilateur Prolog si vous voulez le code source gratuit Rien gratuit car on ne peut que l utiliser sur le web METEOR Logiciel non disponible Minlog Le logiciel Scheme gratuit MINLOG Un compilateur C M
116. simplify use ouldentite2 p p q use equivDef apply ouCommutativite to expression q p V faux V p q simplify apply etCommutativite to expression q p simplify use ReflexiviteDeImplication p p q V p q apply equivIdentitel simplify with disabled RegleDOr implicationDef etCommutativite etAssociativite ouAssociativite ouCommutativite DistOuSurEquiv2 DistOuSurEquiv1 DeMorgan1 DeMorgan2 DistOuSurEt1 DistEtSurOul DistNegSurEquiv1 equivAssociativitel TroisPointSoixanteQuinze fauxDef equivIdentite2 prove 157
117. sion p V q apply ouCommutativite to expression q V p simplify use TroisPointQuaranteDeux4 use TroisPointQuaranteDeuxzA p q q p rewrite apply equivCommutativitel to expression q p V q simplify prove 140 theorem ouExclusif Vp q BoolGries e p q p q V p q proof apply RegleDOr prove use lemme16 p p apply ouCommutativite to expression p V q simplify use lemmel6 p q q p apply DoubleNegation simplify apply ouCommutativite to expression p V q simplify apply ZeroDeOul to expression p V vrai simplify apply equividentite3 to expression vrai p V qz p V qV p simplify apply equividentite3 to expression vrai p V qz p V qV p simplify apply equivCommutativitel to expression q V 7 p vrai simplify apply equivIdentite3 to expression vrai 3 q V p simplify use lemmel6 p q q p apply DoubleNegation simplify apply equivCommutativitel to expression p V q vrai simplify apply equivIdentite3 to expression vrai p V q rewrite apply ouCommutativite to expression p V q simplify use TroisPointQuaranteDeux2 p q q p use TroisPointQuaranteDeux4 p p prove 141 theorem TroisPointSoixanteHuit Vp q r BoolGriesep q r p q r pVq qVre pVr pV avr proof apply RegleDOr simplify apply ouCommutativite to expression p q pVq Vr simplify use DistOuSurEquiv2 p r q p q r p V q use DistOuSurEquiv2 p r q
118. st facilement modifiable 3 4 Il peut recevoir des instructions en notation infix e suffix e ou post Il possede un mode autonome fix e Il fonctionne sur presque toutes les plateformes 6 Sa documentation est int ressante et complete 14 D savantages de Otter 1 2 3 4 Il donne souvent des preuves par contradiction Il a de la difficult trouver des preuves par induction 5a notation laisse d sirer 5a documentation n est pas simple La r solution est une m thode invent e par J A Robinson vers 1960 7 14 4 5 Z EVES Le d monstrateur automatique de th or mes nomm Z EVES est un logi ciel bas sur un syst me automatique de d duction appel NEVER Il conjoint la force du d monstrateur nomm EVES 2 avec le langage de sp cification Z Avantages de Z EVES 1 2 DX 9X Qu m Il tourne sur les plateformes Unix et Windows Il traite seulement de la logique classique notre objectif est de traiter seulement de la logique classique Sa documentation est tr s bien organis e et elle est volumineuse voir 15 16 17 et 18 Son interface est tr s int ressante Ce logiciel est gratuit Il traite de la th orie des ensembles Ses preuves avec la th orie des ensembles ont un bon degr d automa tisme D savantages de Z EVES E 2 3 Il faut avoir une licence pour pouvoir obtenir une version du logiciel Il fonctionne avec une intera
119. stImplicationSurEquiv Vp q r BoolGries ep gt q r p gt q p gt r proof use DefAltDeImplication2 q q r use TroisPointSoizante use equivCommutativitel p p r q p use DefAltDeImplication2 q r prove Ajout de lemme theorem lemme18 Vp q r BoolGrieser V pV q rV ApV pV 7q apy rV 74 proof use lemmel6 p q q p apply ouCommutativite to expression q V p with disabled DistNegSurEquivl DistNegSurEquiv2 equivAssociativite2 ouAssociativite ouCommutativite equivAssociativitel equivCommutativitel equivCommutativites DistOuSurEquiv2 DistOuSurEquiv1 equivIdentite2 prove apply equivCommutativitel to expression r V p V q vrai simplify apply equividentite3 to expression vrai r V p V q simplify apply ouCommutativite to expression r V p V q simplify apply ouAssociativite to expression p V qV r simplify apply ouCommutativite to expression q V r simplify with disabled DistNegSurEquivl DistNegSurEquiv2 equivAssociativite2 ouAssociativite ouCommutativite equivAssociativitel equivCommutativitel equivCommutativites DistOuSurEquiv2 DistOuSurEquiv1 equivIdentite2 prove Fin de l ajout de lemme 144 theorem TroisPointSoixanteDixSept Vp q r BoolGries e p gt q r p q p r proof use DefAltDeImplicationl p q q r use DefAltDeImplicationl g q V r use DefAltDeImplicationl p p gt q q p r use DefAltDeImplicationl g
120. t de voir que votre th or me est v ritablement devenu un th or me pour Z EVES 1Si vous ne d sirez pas que le th or me soit une r gle de r criture omettez simplement le mot rule dans l criture du th or me 48 5 2 8 Formalisme des donn es de sortie Cette section se propose de montrer comment lire une preuve d un th o r me r alis e par notre d monstrateur De plus cette section ne traite que du mode textuel car le mode graphique ne permet pas de voir le d roulement d une preuve avec Z EVES mais permet seulement de connaitre le but cou rant Pour mieux comprendre prenons un exemple simple tir de notre banque de th or mes et faisons le ex cuter par le mode textuel de Z EVES Tout d abord chargeons les axiomes et les th oremes dans Z EVES jusqu au th o reme DistNegSurEquiv4 si vous d sirez r aliser l exemple suivant en m me temps que vous faites la lecture de ce rapport on vous invite lire pr ala blement la section 5 2 9 Ensuite on crit le th oreme DistNegSurEquiv4 de la facon suivante dans l interface Z TEX begin theorem DistNegSurEquiv4 forall p q BoolGries non p equiv q equiv non p q proof reduce apply equivCommutativitel to expression non p equiv q simplify rewrite end theorem Et voila le r sultat donn par Z EVES theorem DistNegSurEquiv4 theorem DistNegSurEquiv4 Beginning proof of DistNegSurEquiv4 p Mn BoolGries NN land q in Bool
121. tOuSurEquiv1 equivAssociativite1 prove apply ouCommutativite to expression p V r V q simplify apply equivCommutativitel to expressionr V 7ng rV7aqV ap simplify apply equivA ssociativite2 to expression 5 p V r rV qV pzrV 0 simplify apply equivCommutativitel to expression o p V r rV qV p simplify 154 theorem TroisPointQuatreVingtOnze suite de la preuve pr c dante V p g t BoolGriese p gt r q r pV q gt r proof apply ouCommutativite to expression p V r simplify apply equivAssociativitelto expressionr V qV Ap rVap TV aq simplify apply ouAssociativite to expression r V q V p simplify apply ouCommutativite to expression a q V p with disabled RegleDOr implicationDef DistOuSurEt1 DistEtSurOul DeMorgan1 DeMorgan2 ouCommutativite ouAssociativite etAssociativite et Commutativite DistNegSurEquiv1 DistOuSurEquiv1 equivAssociativitel prove theorem TroisPointQuatreVingtDouze Vp r BoolGries e p r 2p r r proof apply RegleDOr simplify use DefAltDeImplicationl g r use DefAltDeImplicationl p p q r with disabled implicationDef prove use lemmel6 p r q p apply ouCommutativite to expression p V r simplify with disabled implicationDef prove apply ouCommutativite to expression p V r simplify use TroisPointQuaranteDeux2 p r q p with disabled implicationDef prove 155 theorem ImplicationMutuelle Vp q BoolGries e p gt q q p
122. tan tes globales pour tout le type Ceci se r alise de la mani re suivante begin axdef peutEtre1 BoolGries peutEtre2 BoolGries end axdef Ensuite nous devons d crire le comportement de ces constantes soit avec les constantes d j pr sentes comme la constante faux soit avec les op rateurs d j pr sents comme la constante vrai Nous pourrions d crire une partie du comportement de ces constantes en donnant l axiome suivant begin theorem rule peutEtreiNegation forall p BoolGries non peutEtre1 peutEtre2 end theorem Attention il faut tre extr mement vigilant lorsque nous d finissons de nouvelles constantes Gardons toujours l esprit de v rifier apr s l implan tation des nouvelles constantes si tous les axiomes de base qui concernent de pr s ou de loin ces constantes sont toujours valides car en implantant peut trel et peut tre2 nous venons peut tre de rendre invalide des axiomes et des th or mes de notre banque de th or mes Heureusement tel 69 n est pas le cas avec ces deux nouvelles constantes on peut d montrer que toutes les constantes du type BoolGries r unies dans ce cas ci forment un treillis complet mais cela aurait pu se produire En effet si nous aurions implant plut t la constante peut tre au lieu de peut tre1 et peut tre2 et si nous aurions d fini cette constante l aide de cet axiome begin theorem rule peutEtreNegation forall p
123. tion internal items to p Mn BoolGries NN land q Nin BoolGries NN implies non p equiv q equiv non p q l Dans cette commande on voit que Z EVES simplifie le but courant en utilisant les r gles de r criture Il utilise autant les r gles que nous lui avons donn es que les r gles qu il possede d j Premi rement on voit que Z EVES r crit le but en utilisant l axiome DistNegSurEquiv1 et ensuite l axiome DistNegSurEquiv2 Pour continuer la r duction le d monstrateur automa tique de th or mes utilise des r gles de transfert des th or mes d usage frule qui sont d j dans les outils de Z EVES lorsqu il se charge Ces r gles sont KnownMember declarationPart knowMember et internal items La premiere r gle est en fait une r gle que Z EVES s est cr e partir des d finitions que les concepteurs lui ont donn es Les r gles cr es par Z EVES sont de la forme nom objet ZVA type th or me cr Dans ce cas ci ce th or me vient du sch ma knownMember le th or me cr par le d monstrateur ne contient que la partie de d claration du sch ma Known Member Pour en savoir plus sur les th or mes cr s par Z EVES ils ne sont pas pertinents pour la pr sente recherche lisez 16 surtout la section 3 5 Les internal items sont des objets que nous ne pouvons pas toucher dans Z EVES et qui lui permettent de faire des liens entre les divers op rateurs et pr dicats Ensuite
124. tion Lego Bonne environ 70 pages llprover Tr s basse environ 12 pages METEOR Moyenne abondante mais non structur e Minlog Bonne environ 50 pages MINLOG Basse Ngthm the Boyer Bonne Moore prover Nuprl Tr s bonne abondante et pertinante presque inexistante Oscar Tr s bonne volumineuse compl te et int ressante Fic A 8 Tableau sur les diff rences entre les d monstrateurs automatiques de th oremes suivant les criteres de comparaison qualit de la bibliographie et type d interaction suite 93 qualit de la Type bibliographie d interaction Otter Tr s bonne un livre d instruction complet Script avec plusieurs livre sur la manipulation de Otter Proof General Tr s bonne compl te Editeur et int ressante Prover NP Tools Non trouv e c est un Librairie produit acheter Purr Bonne mais le logiciel Script est encore instable PVS Tr s bonne beaucoup Dialogue i ible bien structur e Saturate Tres bonne compl te Script et int ressante Fic A 9 Tableau sur les diff rences entre les d monstrateurs automatiques de th oremes suivant les criteres de comparaison qualit de la bibliographie et type d interaction suite 94 qualit de la Type bibliographie d interaction SCOTT combinaison Tr s basse sur SCOTT seulement A d Otter et de FINDER SPRFN Basse environ une vingtaine de pages de documentation Watson Tr s bonne compl te et int ressante Z EVES Tr
125. ue la distributivit de la disjonction sur la conjonction Toutes ces transformations permettent de modifier le but pour obtenir un pr dicat compos seulement de conjonctions de disjonctions et de n gations et ayant de plus la conjonction comme op rateur ayant la plus basse pr s ance parmi ceux qui se retrouvent dans l expression Autrement dit cette commande transforme l expression dans la forme normale conjonctive Disjunctive La syntaxe de cette commande est commande disjunctive Le but de cette commande est presque identique a celui de la commande conjunctive sauf que l op rateur ayant la plus basse pr s ance parmi ceux qui se retrouvent dans l expression doit tre la disjonction et non la conjonc tion Autrement dit cette commande transforme l expression dans la forme 11 La forme normale conjonctive est une forme du calcul des propositions o la formule est une conjonction de litt raux disjonctifs ou de clauses 3 32 normale disjonctive Les transformations que la commande effectue sont les m mes que celle de la commande conjunctive sauf pour la derniere trans formation Z EVES applique la distributivit de la conjonction sur la dis jonction la place de la distributivit de la disjonction sur la conjonction 5 2 6 2 Utilisation des th or mes et des d finitions Il y a deux mani res d utiliser les divers th or mes et d finitions dans Z EVES la mani re manuelle et celle a
126. ue q 4 consequence p consequence q 4 et p et q 5 ou V p ou q 5 non non p 9 Maintenant nous avons les op rateurs de la logique propositionnelle de Gries amp Schneider que nous pouvons utiliser mais nous n avons ni leur d finition ni leur comportement L approche que nous avons utilis e consis tait d crire le comportement des op rateurs gr ce aux axiomes de base Cela nous permettait de ne pas tre oblig de d finir chaque op rateur comme tant des combinaisons des op rateurs de base de Z EVES Nous avons donc tendu les op rateurs de Z EVES la logique quationnelle de Gries amp Schnei der Ces op rateurs permettent en conjonction avec des variables de type BoolGries de cr er des expressions dans le langage de Z EVES A ce La syntaxe est donn e en ordre croissant de priorit 8Remarquez bien qu ici le mot expression est employ et non le mot pr dicat 28 moment l on peut cr er des pr dicats avec des expressions et donc donner des th or mes de la logique quationnelle de Gries amp Schneider gr ce cette notation Les axiomes que nous avons implant s sont donn s l annexe B Rendu ce stade ci de la recherche nous avons donc un nouveau type que nous avons appel BoolGries nous avons de nouveaux op rateurs leur priorit leur nombre d arguments et nous avons m me sp cifi leur com portement Nous sommes donc pr ts soumettre des th or
127. uel r alise les preuves de chaque th or me Voici les fichiers qui seront pr sent s dans ce chapitre e ExTheoCourtLogProp tex e ExTheoMoyenLogProp tex e ExTheoLongLogProp tex e Set TheoryZEVES zed lException faite du fichier SetTheoryZEVES zed qui contient plusieurs exemples 2Nous pouvons tout de m me r aliser ces exemples dans le mode textuel il s agit simplement d adapter les commandes qui seront pr sent es dans ce chapitre pour les rendre compatibles dans le mode textuel Les fichiers ne contiennent que les axiomes et les th or mes pertinents pour la d monstration 72 6 1 Exemples sur la logique propositionnelle Premier exemple ExTheoCourtLogProp tex Le premier exemple est celui du fichier ExTheoCourtLogProp tex C est un exemple simple permettant de se faire les dents sur la d monstration de th or mes avec Z EVES Le th or me que nous souhaitons d montrer dans cet exemple est le th oreme Vp q BoolGries ep V qVp p pVq p Tout d abord nous allons charger le fichier ExTheoCourtLogProp tex dans le mode graphique de Z EVES Pour r aliser le chargement de cet exemple dans le mode graphique nous utilisons la m thode expliqu e la section 5 2 9 Apr s avoir charg sans oublier d avoir v rifi syntaxiquement tous les th or mes rendons nous au dernier th or me le th or me TheoremeA De montrer Ensuite cliquons sur le bouton droit de la souris sur le th or
128. utomatique 5 2 6 2 1 La mani re manuelle Il y a trois commandes qu on peut utiliser avec la facon manuelle pour jouer avec les th or mes et les d finitions Ces commandes sont d finies ci dessous Apply Cette commande poss de une syntaxe propre commande apply nom th or me apply nom th or me to expression expression apply nom th or me to predicate pr dicat Le th or me nom th or me doit tre celui que l utilisateur souhaite ap pliquer au but Ce th or me doit tre une r gle de r criture d finie par rule dans la grammaire de Z EVES Une r gle de r criture est un pr dicat contenant deux pr dicats ou deux expressions et ceux ci sont s par s par un signe d galit Lorsque Z EVES rencontre l expression ou le pr dicat de la partie gauche de l galit alors le d monstrateur sait que le c t droit de l galit est quivalent au c t gauche Donc Z EVES peut r crire un pr dicat chaque fois qu il rencontre l expression ou le pr dicat de la partie gauche de l galit en substituant cette partie par la partie droite de l galit Par exemple si le but courant est ce pr dicat Vp q BoolGries e p q p q V p q et qu on poss de la r gle de r criture etCommutativite d finie comme suit Vp q BoolGriesep q q 9p alors notre but devient apr s l ex cution de la commande apply etCommu tativite to expression p q 33 Vp q BoolGries ep q
129. uveau Theoreme Vp q r BoolGries e p implique q ou r p implique q ou p implique r Ensuite vous auriez d r aliser la m me preuve que dans l exemple pr c dent pour que ce th or me soit consid r comme un th or me par Z EVES Pour enlever un th or me De la m me fa on que pour ajouter un th or me il y a deux mani res d enlever un th or me la maniere temporaire et la mani re permanente Encore une fois la mani re permanente est tr s simple vous ditez le fichier contenant l alg bre bool enne dans un diteur de texte supportant IATEX et vous effacez tout simplement ce qui a trait ce th or me dans la banque de donn es Ce coup ci la mani re temporaire ne fonctionne que dans le mode gra phique Il faut simplement une fois que la banque est charg e cliquer avec le bouton droit de la souris sur le th or me dont vous d sirez la mort Ensuite vous s lectionnez la commande Delete dans le menu flottant Finalement sil y avait des th or mes ou des axiomes apr s le th or me que vous venez d enlever ces th or mes et axiomes sont d sactiv s Pour les r activer vous devez les rev rifier syntaxiquement 60 5 2 10 Exemple complet d une d monstration de th o reme Dans cette section nous nous proposons de montrer une d monstra tion compl te d un th or me tape par tape Ce rapport est d j parsem d exemples mais ces exemples sont plut t concentr s sur la mati r
130. y RegleDOr simplify apply DistOuSurEquiv2 simplify apply DistOuSurEquiv2 simplify apply ouCommutativite simplify apply DistOuSurEquiv2 simplify use lemme16 use lemmel6 p q q p apply ouAssociativite to expressionngV p V qV p simplify apply ouCommutativite to expression q V p simplify apply ZeroDeOu1 simplify use equivIdentite5 p p V p q use equivIdentite5 p q V p q use equivIdentite5 p q V a p V p q apply DistOuSurEquiv2 to expression p V p simplify apply DistOuSurEquiv2 to expression q V p q simplify apply DistOuSurEquiv2 to expression q V p V p q simplify apply ouAssociativite to expression q V p V p simplify apply ouCommutativite to expression o q V pV q simplify use TiersExclu2 use TiersExclu2 p q q 139 theorem equivDef suite de la preuve pr c dante Vp q BoolGriesepzq p q V 2p oq proof simplify apply ZeroDeOu1 simplify apply equivIdentite3 to expression vrai p V q apply equividentite3 to expression vrai q V q V p simplify apply equivCommwutativitel to expression q V p vrai simplify apply equivAssociativitel to expression vrai 4 q V p vrai apply equivCommwutativitel to expression q V p vrai simplify apply equivIdentite3 to expression vrai 2 q V p simplify apply ouCommutativite to expression q V p simplify use lemmel6 p p q q apply DoubleNegation simplify apply ouCommutativite to expres

pdf, 708 K - Université Laval

Contents

Download Pdf Manuals

Related Search

Related Contents

pdf, 708 K - Universit&eacute; Laval

Contents

Download Pdf Manuals

Related Search

Related Contents

pdf, 708 K - Université Laval