Search This Blog

25 April 2011

[Coq-Club] formalisation de la logique propositionnelle / introduction to conversational Martian

Bonjour

J'espère que vous êtes conscient que l'enseignant qui vous a donné ce projet a toutes les chances de lire cette mailing liste, et qu'il n'est pas évident qu'il considère que faire corriger/compléter votre
réponse soit exactement le travail qu'il attendait de vous.

J'espère aussi que vous penserez, avant de rendre votre projet, à supprimer le nom de votre camarade Samuel Besset, et à le remplacer
par le votre. Cela risquerait de d'éveiller des soupçons de triche. Ce serait malheureux.

Cordialement,

Alexandre Pilkiewicz

Le 21 avril 2011 11:46, aymen bouslama a écrit:

bonjour,
 
est ce que vous pouvez me dire si c'est juste ce que j'ai fais pour résoudre le problème suivant?
 
Construire un type inductif a deux constructeurs permettant de mod eliser le  fragment implicatif de la logique propositionnelle. Les termes seront soit des  variables, not ees a, b, c, etc. (prises dans un ensemble V ), soit une implication entre deux termes.

On pourra utiliser la biblioth eque String de Coq pour g erer les noms des propositions.

Interpretation On propose de repr esenter une valuation par une liste de paires (variable,bool een).

Definition valuation := list (string * bool).

Ecrire une fonction list assoc qui, etant donn ee une variable  propositionnelle et une valuation V donne la valeur de la variable dans la valuation.

Ex : si
 V=[("x",true);("y", false)] list_assoc V y=false.

 Ecrire une fonction d'interpr etation qui, etant donn e une formule F et  une valuation I, calcule si I satisfait F , i.e. I(F ) = true.

Tables de v erit e Programmer une fonction qui prend en argument un terme du calcul propositionnel et calcule s'il s'agit d'une tautologie ou non en utilisant une table de v erit e.

Indication : on pourra enum erer toutes les valuations possibles. Il su ra ensuite de tester que la formule est satisfaite pour toutes ces valuations. On pourra pour cela utiliser les fonctions d'ordre sup erieurs sur les listes (par exemple forallb). Pour l'implication (2 variables), le nombre de cas a etudier pour d eterminer si on a a faire a une tautologie est 4.

 Utiliser votre fonction pour v eri er que les termes suivants sont bien des tautologies.

 { Pierce : ((A - B) -A) -A
 { S : F -(G - F )
 { K : (F - (G - H)) - ((F - G) - (F - H))
 -------------------------------

 (*---------------------------------------------------------------------------------*)
 (*------------------------------ PROJET COQ M1 ILC
 --------------------------------*)
 (*------------------------------ BESSET SAMUEL
 --------------------------------*)
 (*---------------------------------------------------------------------------------*)
 Require Export List.
 Require Export String.
 Require Export Bool.
 Open Local Scope char_scope.
 (*---------------------------------------------------------------------------------*)
 (* Formaliser la syntaxe et sémantique et modéliser un système de déduction
 *)
 (*---------------------------------------------------------------------------------*)

 (*---------------------------------------------------------------------------------*)
 (*
 SYNTAXE *)
 (*---------------------------------------------------------------------------------*)

 (* Définition inductive du type : form *)
 Inductive form : Set :=
 | p : string - form (* proposition *)
 | i : form - form - form (* implication *)
 | e : form - form - form (* ET logique *)
 | o : form - form - form (* OU logique *)
 .
 (*---------------------------------------------------------------------------------*)
 (*
 SEMANTIQUE *)
 (*---------------------------------------------------------------------------------*)

 (* Définition de la valuation *)
 Definition valuation := list (string * bool).

 (* Définition de la fonction : list_assoc *)
 Fixpoint list_assoc a (v:valuation) : bool :=
 match v with
 | nil = false
 | (x,b) :: l =
 if string_dec x a then b
 else list_assoc a l
 end.

 (* Définition de la fonction : interpretation *)
 Fixpoint interpretation form (v:valuation) : bool :=
 match form with
 | p s1 = list_assoc s1 v
 | i form1 form2 = (orb (negb (interpretation form1 v)) (interpretation
 form2 v))
 | e form1 form2 = (andb (interpretation form1 v) (interpretation form2
 v))
 | o form1 form2 = (orb (interpretation form1 v) (interpretation form2 v))
 end.

 (*---------------------------------------------------------------------------------*)
 (* TEST -
 SEMANTIQUE *)
 (*---------------------------------------------------------------------------------*)

 (* Tests des définitions précédentes : *)
 Definition a := (String "A" EmptyString).
 Definition b := (String "B" EmptyString).
 Definition val := (a,true)::(b,false)::nil.

 Eval compute in (interpretation (p a) val). (* doit rendre : true *)
 Eval compute in (interpretation (p b) val). (* doit rendre : false *)
 après avez vous une idée pour la suite?
 Syst eme formel
 On rappelle les r egles de la d eduction naturelle : comme elim et intro
 On d eclare un contexte (comme ) comme une liste de formules.
 Definition context := list formule.
 1. Mod eliser le syst eme formel pr ec edent a travers un type inductif de la forme :
 Inductive prouvable : context - formule - Prop := ...
 2. Prouver ensuite le th eor eme A - A dans ce syst eme.
3. Faire de m^eme avec les th eor emes S et K de la section pr ec edente.
4. On va maintenant s'int eresser a la preuve de la correction de ce systeme formel.
(a) D e nir un pr edicat consequence_l qui prend en argument un contexte et une  formule F et indique si F est cons equence s emantique de .
(b) Prouver le th eor eme suivant :
Lemma correctness : forall P G,
provable G P - consequence_l G P.

 merci
 Cordialement

6 comments:

Unknown said...

bonjour,

oui je sais bien que l'enseignant peut bien lire ça et alors?
c'est quoi la différence entre ce que j'ai fais et de chercher sur internet
et pour vous dire j'ai aussi contacté d'autre prof dans d'autres établissement
je pense que de chercher a comprendre c'est mieux de ne rien rendre
et je sais bien que j'ai envoié l'email avec le nom de mon camarade
vu que j'ai travaillé sur le sien.
la triche ?? si c'était de la triche j'aurais changé le nom comme vous avez dis
de plus j'ai bien utilisé mon nom est ce que vous pensez que si j'étais pas honête je laisserais mon nom et le nom de mon camarade??
vous me répondez comme si c'est pas moi qui a envoié l'email ..
c'est moi qui l'as envoié et je sais ce que j'ai écris dedans..

merci comme même
Cordialement

Anonymous said...

I’m kninda bored, I’m Swiss, therefore I can speak french (amongst about 3 other lingos) so here we go with the translation. No TranslationBot was required or harmed during this effort, just thank the swiss school system where french is mantatory:

Hello
Yes I know that the professor is well able to read this, so what ?
What is the difference between what I did and searching on the Internet and just to tell you / let you know I have also contacted other professors from various instituions. I thought that trying to understand / comprehend than to do nothing
and I am well aware that I sent this email under the name of my colleague while working on his machine
Trick ? If this was a trick then I had changed the name just like you advised.
What’s more I would have used my name would you think that I was not honest I would have left my name and the name of my colleague ?
You reply to me like I was not the person who sent this email.
It was me who sent it, I know because I wrote the content / what was in there

thanks anyway
rgds

PatFromCH said...

ah bugger, forgot to leave my name

Vleeptron Dude said...

aymen and PatFromCH --

SVP cliquez ici:

http://vleeptronz.blogspot.com/2011/04/my-philosophy-professor-leo-rauch.html

(the newest Vleeptron post)

PatFromCH said...

this is the beginning of the mail:

Hello
I hope you are aware that the professor who gave you this project has all the possiblities to read this mailing list and that it is not at all sure / obvious that he will correct / complete the piece of work he has been expecting from you

I also hope that before you return your project to delete the name of your colleague Samuel Besset and replace it with yours in order to avoid any trickery which would be very unfortunate

rgds
Alexandre Pilkiewicz

On 21/4/11 ayan wrote:

Hello
Can you please tell me if what I have done to solve the following problem is correct ?

(What follows is a mathematical problem. Let me get my head around that first, this is higly specialized and difficult to translate)

Gabriella said...

It will not succeed as a matter of fact, that is what I consider.