Bonjour, Juste un petit mail pour faire un peu de clarté concernant le planning de demain : - 10h : on se voit tous en B107 pour une micro-séance de TP Coq (correction de l'exo 1 de Micaela) ; - 10h30 (ou quelques minutes avant) : on observe l'éclipse ; - 11h (ou quelques minutes après) : on se retrouve tous de nouveau en B107 pour le séminaire de Charles Grellois. Amicalement, Damiano PS : je ne pourrai pas assister au séminaire, Domenico s'occupera de l'organisation.
Bonjour, Comme je l'avais dit à Pierre et à Damiano, je ne serai pas là car je vais rester avec ma fille pour l'éclipse, et comme je dois venir pour travailler (sans être trop interrompus) l'après-midi, je ne peux pas l'ammener au labo. Par contre, pour l'exo 1 du TD1, comme je l'avais dit à Pierre et Damiano, il faut que vous commenciez par avoir la preuve papier (ou dans la tête) très clairement. C'est comme lorsque vous écrivez un programme, si vous avez l'algo c'est mieux ;-) Pour faire la preuve il faut commencer par eliminer A\/~A avec A=rac(2)^rac(2) est rationnel. Ensuite, suivant que vous êtes dans le cas gauche ou droit, vous donnez les valeurs adéquates à x et y. a+, /MM. On Thu, 19 Mar 2015, Damiano Mazza wrote:
Bonjour,
Juste un petit mail pour faire un peu de clarté concernant le planning de demain :
- 10h : on se voit tous en B107 pour une micro-séance de TP Coq (correction de l'exo 1 de Micaela) ; - 10h30 (ou quelques minutes avant) : on observe l'éclipse ; - 11h (ou quelques minutes après) : on se retrouve tous de nouveau en B107 pour le séminaire de Charles Grellois.
Amicalement,
Damiano
PS : je ne pourrai pas assister au séminaire, Domenico s'occupera de l'organisation.
_______________________________________________ Gdtlogprog mailing list Gdtlogprog@lipn.univ-paris13.fr https://www-lipn.univ-paris13.fr/mailman/listinfo/gdtlogprog
---------------------------------------- Micaela.Mayero@lipn.univ-paris13.fr http://www-lipn.univ-paris13.fr/~mayero/
Le 19 mars 2015 à 19:09, Micaela Mayero <mayero@lipn.univ-paris13.fr> a écrit :
Par contre, pour l'exo 1 du TD1, comme je l'avais dit à Pierre et Damiano, il faut que vous commenciez par avoir la preuve papier (ou dans la tête) très clairement. C'est comme lorsque vous écrivez un programme, si vous avez l'algo c'est mieux ;-)
Pour faire la preuve il faut commencer par eliminer A\/~A avec A=rac(2)^rac(2) est rationnel. Ensuite, suivant que vous êtes dans le cas gauche ou droit, vous donnez les valeurs adéquates à x et y.
Pour ceux qui voudraient finir l’exercice mais qui butent sur les tactiques, voici la liste de celles que j’ai utilisé : - exists, qui permet d’introduire un témoin d’existence (utilisation «exists t») - elim, qui fait toutes les éliminations en déduction naturelle - split, qui casse les conjonctions dans les buts en plusieurs sous-buts (\with-intro) - exact, qui permet d’utiliser une hypothèse globale (utilisation «exact hyp») - assumption, la règle identité - apply, qui remonte le long d’une implication - rewrite, qui ré-écrit le long d’une égalité, orientée de gauche à droite (utilisation «rewrite hyp», où hop est de la forme a=b) Je ne prétends pas que ce soit optimal ou quoi que ce soit :) À demain, — Luc
Bonsoir, Finalement, demain je retire mes enfants de l'école parce qu'autrement ils y seraient cloitrés dans un couloir sans fenêtre toute la matinée. C'est bien la première fois que j'en suis réduit à ces extrémités. Je ferai donc un peu de Coq, un peu d'eclipse (mais pas la java), si possible en compagnie de scientifiques, et tout le séminaire par les bonnes grâces de la précarité de l'emploi. Bonne soirée, Pierre Le 19/03/2015 18:47, Damiano Mazza a écrit :
- 10h : on se voit tous en B107 pour une micro-séance de TP Coq (correction de l'exo 1 de Micaela) ; - 10h30 (ou quelques minutes avant) : on observe l'éclipse ; - 11h (ou quelques minutes après) : on se retrouve tous de nouveau en B107 pour le séminaire de Charles Grellois.
Bonjour, finalement, je me trouve dans la pénible situation de Pierre et je suis forcé à rester à la maison pour empêcher que mon fils soi enfermé toute la matinée dans une couloir sans fenêtre, en attendant sans soute la fin du monde ou en espérant que les mauvais signes envoyé par le dieux soleil qui a décidé de se caché ne soit trop néfastes. Je prie l'orateur de m'en excuser. Bien cordialement --s PS Pour plus de detail, voici un intéressant commentaire: http://www.lemonde.fr/sciences/article/2015/03/19/eclipse-non-a-l-obscuranti... Pour continuer à espérer que l'école ne soit pas esclave des compétences à apprendre et des "pesudo-résultats", mais un lieu de stimule de la curiosité et de l'analyse de la réalité physique, ou plus en générale scientifique, et du contexte sociale qui nous entoure. ===================================== Stefano Guerrini Institut Galilée, Université Paris 13, Sorbonne Paris Cité Laboratoire d'Informatique de Paris-Nord (LIPN) stefano.guerrini@univ-paris13.fr
On 19 mars 2015, at 21:33, Pierre Boudes <boudes@univ-paris13.fr> wrote:
Bonsoir,
Finalement, demain je retire mes enfants de l'école parce qu'autrement ils y seraient cloitrés dans un couloir sans fenêtre toute la matinée. C'est bien la première fois que j'en suis réduit à ces extrémités.
Je ferai donc un peu de Coq, un peu d'eclipse (mais pas la java), si possible en compagnie de scientifiques, et tout le séminaire par les bonnes grâces de la précarité de l'emploi.
Bonne soirée, Pierre
Le 19/03/2015 18:47, Damiano Mazza a écrit :
- 10h : on se voit tous en B107 pour une micro-séance de TP Coq (correction de l'exo 1 de Micaela) ; - 10h30 (ou quelques minutes avant) : on observe l'éclipse ; - 11h (ou quelques minutes après) : on se retrouve tous de nouveau en B107 pour le séminaire de Charles Grellois.
!DSPAM:78,550b3299221847490478932!
Bonjour, On Fri, 20 Mar 2015 08:43:00 +0100, Stefano Guerrini <stefano.guerrini@univ-paris13.fr> wrote:
Bonjour,
finalement, je me trouve dans la pénible situation de Pierre et je suis forcé à rester à la maison pour empêcher que mon fils soi enfermé toute la matinée dans une couloir sans fenêtre, en attendant sans soute la fin du monde ou en espérant que les mauvais signes envoyé par le dieux soleil qui a décidé de se caché ne soit trop néfastes.
il faut bien dire que les risques ne sont pas négligeables : http://www.legorafi.fr/2015/03/18/les-choses-a-savoir-sur-leclipse-partielle... « Les Frères Bogdanov vont-ils être encore invités pour expliquer le phénomène ? Oui, à 8h sur BFMTV, 8h12 sur France Inter, 8h30 sur iTélé, 8h40 sur Mouv’, 8h42 sur LCI, 9h sur Europe1, 9h08 sur France Info, 9h12 sur OuiFM, 9h30 sur Skryrock, 9h47 sur France Culture, 10h04 sur RTL2, 10h25 sur Radio Classique, et en invités spéciaux dans le Grand Journal sur Canal Plus à 19h00. » J'en frémis d'horreur rien qu'à y penser…
Je prie l'orateur de m'en excuser.
Bien cordialement
--s
PS Pour plus de detail, voici un intéressant commentaire:
http://www.lemonde.fr/sciences/article/2015/03/19/eclipse-non-a-l-obscuranti...
-- Cordialement, Jean-Yves Moyen
Bonjour, pour ceux qui ne sont pas (encore) en séminaire, toute la magie de l’internet peut vous permettre de voir tout de même un peu ce qui se passe : http://www.dailymotion.com/video/x2jr6o5_pic-du-midi-hautes-pyrenees_tv <http://www.dailymotion.com/video/x2jr6o5_pic-du-midi-hautes-pyrenees_tv> Amicalement, Bon modèle infinitaire de la Logique Linéaire à vous tous ! Clément.
Le 20 mars 2015 à 09:39, Jean-Yves Moyen <Jean-Yves.Moyen@lipn.univ-paris13.fr> a écrit :
Bonjour,
On Fri, 20 Mar 2015 08:43:00 +0100, Stefano Guerrini <stefano.guerrini@univ-paris13.fr> wrote:
Bonjour,
finalement, je me trouve dans la pénible situation de Pierre et je suis forcé à rester à la maison pour empêcher que mon fils soi enfermé toute la matinée dans une couloir sans fenêtre, en attendant sans soute la fin du monde ou en espérant que les mauvais signes envoyé par le dieux soleil qui a décidé de se caché ne soit trop néfastes.
il faut bien dire que les risques ne sont pas négligeables : http://www.legorafi.fr/2015/03/18/les-choses-a-savoir-sur-leclipse-partielle...
« Les Frères Bogdanov vont-ils être encore invités pour expliquer le phénomène ? Oui, à 8h sur BFMTV, 8h12 sur France Inter, 8h30 sur iTélé, 8h40 sur Mouv’, 8h42 sur LCI, 9h sur Europe1, 9h08 sur France Info, 9h12 sur OuiFM, 9h30 sur Skryrock, 9h47 sur France Culture, 10h04 sur RTL2, 10h25 sur Radio Classique, et en invités spéciaux dans le Grand Journal sur Canal Plus à 19h00. »
J'en frémis d'horreur rien qu'à y penser…
Je prie l'orateur de m'en excuser.
Bien cordialement
--s
PS Pour plus de detail, voici un intéressant commentaire:
http://www.lemonde.fr/sciences/article/2015/03/19/eclipse-non-a-l-obscuranti...
-- Cordialement, Jean-Yves Moyen _______________________________________________ Seminairelcr mailing list Seminairelcr@lipn.univ-paris13.fr https://www-lipn.univ-paris13.fr/mailman/listinfo/seminairelcr
INRIA — Université Paris-Est, LACL (EA 4219), UPEC clement.aubert@lacl.fr <mailto:clement.aubert@lacl.fr> http://lacl.fr/~caubert/ <http://lacl.fr/~caubert/>
participants (7)
-
"Clément Aubert (CNRS)" -
Damiano Mazza -
Jean-Yves Moyen -
Luc Pellissier -
Micaela Mayero -
Pierre Boudes -
Stefano Guerrini