Hello!

Inspiré(e) de prendre part à la discussion ? Ou de poser une question ou demander de l’aide ?

Alors bienvenues dans les grands sujets des forums de La Bulle : m’inscrire.

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
Avatar de l’utilisateur
  • Genre : Télétubbie
  • Messages : 15405
Dim 29 Oct 2017 12:02
Message 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.

Image
Hibou57

« La perversion de la cité commence par la fraude des mots » [Platon]
Profil Site Internet
Administrateur
Avatar de l’utilisateur
  • Genre : Télétubbie
  • Messages : 15405
Lun 30 Oct 2017 02:22
Message Re: Les logiques : notes en vrac
Le terme « théorème » est malheureusement parfois utilisé quand il s’agit d’axiome.

Image
Hibou57

« La perversion de la cité commence par la fraude des mots » [Platon]
Profil Site Internet
Administrateur
Avatar de l’utilisateur
  • Genre : Télétubbie
  • Messages : 15405
Jeu 24 Mai 2018 18:04
Message 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!
Must be combined with testing


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.

Image
Hibou57

« La perversion de la cité commence par la fraude des mots » [Platon]
Profil Site Internet
Administrateur
Avatar de l’utilisateur
  • Genre : Télétubbie
  • Messages : 15405
Jeu 24 Mai 2018 21:21
Message Re: Les logiques : notes en vrac
Trois concepts à aborder :

  • Program analysis (analyse de programme).
  • Model checking (vérification de modèle).
  • Abstract interpretation (interprétation abstraite).

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.

Image
Hibou57

« La perversion de la cité commence par la fraude des mots » [Platon]
Profil Site Internet
Administrateur
Avatar de l’utilisateur
  • Genre : Télétubbie
  • Messages : 15405
Jeu 24 Mai 2018 23:44
Message 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.

Image
Hibou57

« La perversion de la cité commence par la fraude des mots » [Platon]
Profil Site Internet
Administrateur
Avatar de l’utilisateur
  • Genre : Télétubbie
  • Messages : 15405
Ven 25 Mai 2018 13:26
Message 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é.

Image
Hibou57

« La perversion de la cité commence par la fraude des mots » [Platon]
Profil Site Internet
Administrateur
Avatar de l’utilisateur
  • Genre : Télétubbie
  • Messages : 15405
Ven 25 Mai 2018 14:41
Message 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.

Image
Hibou57

« La perversion de la cité commence par la fraude des mots » [Platon]
Profil Site Internet
Administrateur
Avatar de l’utilisateur
  • Genre : Télétubbie
  • Messages : 15405
Ven 25 Mai 2018 15:47
Message Re: Les logiques : notes en vrac
Ces termes anglophones, semblent être synonymes :

  • Formal system ;
  • Logical calculi ;
  • Logical system.

Un système logique (je préfère cette expression) est composé de :

  • Un alphabet, qui est un ensemble fini de symboles.
  • Une grammaire, définissant comment construire une formule bien formée (il y en a typiquement une infinité).
  • Un ensemble de règles d’inférence qui sont souvent elles‑mêmes des formules valides selon la grammaire, mais pas toujours.
  • Un ensemble d’axiomes qui sont eux‑mêmes des formules valides selon la grammaire (un axiome est souvent comme une règle d’inférence sans prémisse, mais pas toujours).

Un système logique a les propriétés (vérifiées ou non) suivantes :

  • Consistency (cohérence) ;
  • Validity (validité) ;
  • Completeness (complétude) ;
  • Soundness (solidité ou correction).

Image
Hibou57

« La perversion de la cité commence par la fraude des mots » [Platon]
Profil Site Internet
Administrateur
Avatar de l’utilisateur
  • Genre : Télétubbie
  • Messages : 15405
Sam 26 Mai 2018 01:03
Message 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.

Image
Hibou57

« La perversion de la cité commence par la fraude des mots » [Platon]
Profil Site Internet
Administrateur
Avatar de l’utilisateur
  • Genre : Télétubbie
  • Messages : 15405
Sam 26 Mai 2018 11:47
Message 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.

Image
Hibou57

« La perversion de la cité commence par la fraude des mots » [Platon]
Profil Site Internet