Cette partie du forum n’est pas compatible avec les bloqueurs publicitaires
Félicitations à vous, de préférer les accès payants plutôt que la gratuité par la publicité, c’est honnorable et cohérent de votre part. Malheureusement, l’accès payant par micropaiement (qui serait d’environ 1 cent pour 20 pages consultées) n’est pour l’instant pas encore mis en place, et l’accès gratuit sans publicité, est réservé aux membres actif(ve)s du forum. En attendant, si vous souhaitez poursuivre votre visite chez nous, vous pouvez ajouter le site à votre liste blanche, ou encore mieux, désactiver le bloqueur partout. Pour ajouter le site à votre liste blanche, pour Firefox (similaire pour les autres navigateurs), rendez‑vous en bas à gauche de la fenêtre de votre navigateur, et cliquez sur le menu comme dans l’exemple de l’image ci‑dessous, puis rechargez la page, en appuyant sur F5.
Les logiques : notes en vrac
|
|
|
| Auteur | Message |
|---|---|
|
Administrateur
|
Mar 29 Avr 2014 02:12
Re: Les logiques : notes en vrac
Peut‑être une différence qui distingue clairement la sémantique axiomatique ou la dénotationnelle de la sémantique opérationnelle…
Si j’écris par exemple 1/0 - 1/0, chacune des deux divisions ne peut être calculée, mais la différence peut l’être symboliquement, et le résultat me semble pouvoir être 0 (mais ça dépend probablement aussi de l’interprétation du résultat). Sûrement que pour la sémantique opérationnelle, cette expression est toujours invalide, tandis qu’elle peut l’être pour la sémantique axiomatique ou la dénotationnelle. Est‑ce ça la différence ? Ou peut‑être un exemple de différence et qu’il y en a d’autres… Il faudra d’ailleurs que je poste un message dédié aux différentes formes de sémantiques, mais pas encore assez de matière pour le moment.  Hibou57 « La perversion de la cité commence par la fraude des mots » [Platon] |
 
|
|
|
|
|
|
Administrateur
|
Mar 24 Juin 2014 09:32
Re: Les logiques : notes en vrac
Un article qui essaie d’expliquer pourquoi la pratique des preuves formelles, qui auraient dut être vues comme d’une évidente nécessité depuis les débuts de l’informatique, ne se sont pas vu attribuées leurs places jusque maintenant. L’auteur suppose que la situation pourrait changer à l’avenir.
Lire : Formal methods start to add up again (computing.co.uk). Janvier 2004. Auteur non‑mentionné. Hibou57 « La perversion de la cité commence par la fraude des mots » [Platon] |
|
|
|
|
Administrateur
|
Mer 25 Juin 2014 08:31
Re: Les logiques : notes en vracHibou a écrit :
Il y a encore plus de types de sémantiques que ça. Programming Language Semantics (cs.ucf.edu) [PDF]. David A. Schmidt, Kansas State University, 2012. Chapitre 6 a écrit :
Hibou57 « La perversion de la cité commence par la fraude des mots » [Platon] |
|
|
|
|
Administrateur
|
Jeu 26 Juin 2014 08:37
Re: Les logiques : notes en vracHibou a écrit : Il y a encore plus de types de sémantiques que ça. Apparemment, des types de sémantiques par domaines ou par logiques. Deux autres, spécifiques à la logique du second ordre : sémantique standard et sémantique de Henkin. La logique du premier ordre, n’a qu’une sémantique, la sémantique standard. Hibou57 « La perversion de la cité commence par la fraude des mots » [Platon] |
|
|
|
|
Modératrice
|
Jeu 26 Juin 2014 18:26
Re: Les logiques : notes en vrac A chaque fois que je passe par ici je me demande si tu parles français. A chaque fois que je passe par ici je tire la même tête et je repars.
|
|
|
|
|
Administrateur
|
Jeu 26 Juin 2014 20:15
Re: Les logiques : notes en vraczen a écrit : A chaque fois que je passe par ici je me demande si tu parles français. Tout n’est pas encore clair pour moi non‑plus  .J’essaie de baliser un sujet. Je le fais sur le forum, parce que c’est pas plus inapproprié que de prendre des notes tout seul dans un fichier texte, et aussi au cas où ça intéresse quelques rares gens de passage, qui pourraient aussi peut‑être vouloir faire remarquer des erreurs. Hibou57 « La perversion de la cité commence par la fraude des mots » [Platon] |
|
|
|
|
Administrateur
|
Lun 30 Juin 2014 09:41
Re: Les logiques : notes en vrac
Ce sujet qui essaie de baliser le vaste thème de la logique, appliquée à l’informatique et aux preuves de fiabilité des logiciels, suppose à priori, que l’usage de démonstrations qu’une implémentation satisfait une spécification, est une bonne chose.
Ci‑dessous, un article qui met en question cet à priori. Il le fait néanmoins en se posant des questions seulement sur le rapport qualité / cout, et non‑pas en mettant en question le bénéfice de s’assurer par des démonstrations, un bénéfice que l’auteur de la question juge indiscutable… il s’interroge donc seulement sur le cout, cependant aussi sur les — pressenties faibles — opportunités d’adoption de cette manière de concevoir les logiciels. On the — Alleged — Value of Proof for Assurance (lambda-the-ultimate.org). Mars 2010. Hibou57 « La perversion de la cité commence par la fraude des mots » [Platon] |
|
|
|
|
Administrateur
|
Lun 30 Juin 2014 21:24
Re: Les logiques : notes en vrac
Il a surtout été question de HOL, à cause de la correspondance de Curry‑Howard, dont découle directement cette logique (HOL, c’est typiquement un modèle du lambda calcul simplement typé). Mais ce n’est pas la seule, il existe le Calcul des Construction (Calculus of Construction — CoC), sur lequel repose le système de démonstration Coq.
Deux documents intéressant établissant une relation et une comparaison des deux. Le premier compare les systèmes HOL en général et le système Coq. Le second, discute d’une interprétation de HOL dans Coq. Je me demande par ailleurs si on peut aussi interpréter Coq dans HOL, ou si Coq est plus expressif que HOL sans tenir compte des aspects pratiques (les types dépendants par exemple, pratiques, et non directement disponibles avec HOL). J’essaierai d’en savoir plus à ce sujet, plus tard. A comparative study of Coq and HOL (kar.kent.ac.uk) [PDF]. Vincent Zammit. 2009. Interpreting HOL in the Calculus of Constructions (people.uleth.ca) [PDF]. Jonathan P. Seldin. 2004. Hibou57 « La perversion de la cité commence par la fraude des mots » [Platon] |
|
|
|
|
Administrateur
|
Lun 30 Juin 2014 21:58
Re: Les logiques : notes en vrac
Interestingly, il semble exister deux versions de la logique intuitionniste : la logique intuitionniste « normale », la version dite « forte », et une version Russe de la logique intuitionniste, semblant être moins fiable.
Je le tiens d’un commentaire à cette question : How true are theorems proved by Coq? (mathoverflow.net). Mars 2011. Commentaire à la question a écrit :
As far as I have been taught, Coq proofs are pretty much the best proofs you can get: they just require intuitionistic logic in the strong sense (not the Russian one). […] Hibou57 « La perversion de la cité commence par la fraude des mots » [Platon] |
|
|
|
|
Débateur
 
|
Mar 1 Juil 2014 16:56
Re: Les logiques : notes en vrac
Sincèrement Ô
 ,J'ai essayé de suivre mais je suis largué ! J'avais eu bien difficile il y a quelques années comprendre les bases de la logique booléenne, à ce jour soit 15 ans plus tard, non seulement je ne m'en souviens que très peu mais j'ai grand mal à comprendre, que dis-je. . . je n'arrive pas du tout à comprendre ce que tu as écrit dans les pages précédentes, pardonnes-moi, mon quotient intellectuel est vraiment trop bas pour suivre. 
 ....Je suis de là-bas ! |
|
|
|
|
|
|
