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
|
Dim 29 Oct 2017 12:02
Re: Les logiques : notes en vrac
La différence entre un théorème et une démonstration, c’est que la démonstration est un théorème potentiel, et ne peut être « convertie » en théorème qu’après validation.
 Hibou57 « La perversion de la cité commence par la fraude des mots » [Platon] |
 
|
|
|
|
|
|
Administrateur
|
Lun 30 Oct 2017 02:22
Re: Les logiques : notes en vrac
Le terme « théorème » est malheureusement parfois utilisé quand il s’agit d’axiome.
Hibou57 « La perversion de la cité commence par la fraude des mots » [Platon] |
|
|
|
|
Administrateur
|
Jeu 24 Mai 2018 18:04
Re: Les logiques : notes en vrac
Une citation importante, de Program verification using Hoare logic (inf.ed.ac.uk), Petros Papapanagiotou, 2013-2016.
Petros Papapanagiotou a écrit : • Formally verified programs may still not work! Il existe en effet et malheureusement, une croyance selon laquelle, quand on utilise des preuves de fonctionnement, on a plus besoin de tests. Cette croyance est répandue chez les gens qui n’ont pas d’expérience dans les preuves ou qui n’ont pas l’intuition de ce qu’elles sont. Une spécification peut signifier autre chose que ce que l’humain croit comprendre. L’inconsistance de Pollack en est un peu un exemple particulier. Une spécification peut être mal posée ou mal comprise, même si sa formalisation est bien comprise. Une spécification peut être partielle, ne pas couvrir tout le programme ou toute la réalité pratique. Hibou57 « La perversion de la cité commence par la fraude des mots » [Platon] |
|
|
|
|
Administrateur
|
Jeu 24 Mai 2018 21:21
Re: Les logiques : notes en vrac
Trois concepts à aborder :
Et aussi, clarifier la différence entre analyse de programme et vérification de modèle, parce que je le comprends comme si la vérification de modèle était un cas particulier d’analyse de programme, alors que les deux semble être distinctes. Hibou57 « La perversion de la cité commence par la fraude des mots » [Platon] |
|
|
|
|
Administrateur
|
Jeu 24 Mai 2018 23:44
Re: Les logiques : notes en vrac
Les deux grandes familles de logiques les plus courantes, sont les logiques provenant de la théorie des ensembles et les logiques provenant de la théorie des types.
Je crois que la logique classique tient surtout de la première, la théorie des ensembles. Ce qui me le fait penser, c’est que je me souviens qu’à l’école primaire, une certaine importance était donnée à l’instruction de la notion d’ensemble et d’opération sur les ensembles. Une autre chose, est que dans la théorie des ensembles, les connecteurs logiques sont des choses distinctes de la notion d’ensemble, tandis que dans la théorie des types, les connecteurs logiques sont des types et dans la culture populaire, les connecteurs logiques appartiennent à une domaine autre que ce sur quoi on les applique. Hibou57 « La perversion de la cité commence par la fraude des mots » [Platon] |
|
|
|
|
Administrateur
|
Ven 25 Mai 2018 13:26
Re: Les logiques : notes en vrac
Un livre intéressant, surnommé « la Bible » dans certains milieux, est “ The lambda calculus, its syntax and semantics ” de H.P. Barendregt. Mais il est cher, alors mieux vaut chercher dans l’occasion. Faire attention aussi à l’édition, comme il en existe plusieurs éditions.
Attention aussi au fait que ce livre semble surtout traiter du lambda calcul non‑typé. Hibou57 « La perversion de la cité commence par la fraude des mots » [Platon] |
|
|
|
|
Administrateur
|
Ven 25 Mai 2018 14:41
Re: Les logiques : notes en vrac
Un wiki sur les mathématiques, la physique et la philosophie, qui a des entrées concernant les logiques : ncatlab.org.
Hibou57 « La perversion de la cité commence par la fraude des mots » [Platon] |
|
|
|
|
Administrateur
|
Ven 25 Mai 2018 15:47
Re: Les logiques : notes en vrac
Ces termes anglophones, semblent être synonymes :
Un système logique (je préfère cette expression) est composé de :
Un système logique a les propriétés (vérifiées ou non) suivantes :
Hibou57 « La perversion de la cité commence par la fraude des mots » [Platon] |
|
|
|
|
Administrateur
|
Sam 26 Mai 2018 01:03
Re: Les logiques : notes en vrac
Pour comprendre HOL, je recommande cette lecture : Higher‑order logic (tuwien.ac.at) [PDF], Stefan Hetzl, 2017. Il explique simplement le passage de la logique du premier ordre à la logique d’ordres supérieurs.
Elle est aussi ajoutée à la bibliographie à la deuxième page de ce sujet. Hibou57 « La perversion de la cité commence par la fraude des mots » [Platon] |
|
|
|
|
Administrateur
|
Sam 26 Mai 2018 11:47
Re: Les logiques : notes en vrac
Il y a deux définitions de l’égalité entre deux fonctions dans le lambda calcul utilisé comme système déductif. La première, dite en intention, tient pour égales deux fonctions qui mises sous formes canoniques, ont la même structure. La deuxième, dite en extension, tient pour égales deux fonctions qui établissent la même correspondance (leur application).
Les deux, en intention et en extension, ne sont pas nécessairement équivalente, elles peuvent différer selon le typage (non‑typé, simplement typé, polymorphique, etc). En Anglais ont dit Intensional lambda calculus et Extensional lambda calculus. Hibou57 « La perversion de la cité commence par la fraude des mots » [Platon] |
|
|
|
|
|
|
