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 : 15514
Lun 28 Déc 2015 20:47
Message Re: Les logiques : notes en vrac

Les dix règles d’inférence du standard OpenTheory (gilith.com)


Et OpenTheory, repose sur HOL …

Source de ce qui suit : The OpenTheory Standard Theory Library (gilith.com) [PDF], Joe Hurd, Avril 2011.

refl t: ∴ ⊢ t = t
(une chose est égale à elle‑même)

assume ϕ: ∴ {ϕ} ⊢ ϕ
(une prémisse est considérée comme un fait connu)

eqMp: Γ ⊢ ϕ = ψ, Δ ⊢ ϕ ∴ Γ ∪ Δ ⊢ ψ
(si dans un contexte on sait que deux certaines choses sont égales, si dans autre contexte on sait la première chose, alors dans l’union des deux contextes, on sait la deuxième chose)

absThm v: Γ ⊢ t = u ∴ Γ ⊢ (λv.t) = (λv.u)
(deux expressions égales se substituent l’une/l’autre comme corps d’une fonction)

appThm: Γ ⊢ f = g, Δ ⊢ x = y ∴ Γ ∪ Δ ⊢ f x = g y
(si deux fonctions sont égales, si deux expressions sont égales, alors l’application de ces deux fonctions à l’une de ces deux expressions, donne deux expressions égales)

deductAntisym: Γ ⊢ ϕ, Δ ⊢ ψ ∴ (Γ - {ψ}) ∪ (Δ - {ϕ}) ⊢ ϕ = ψ

subst σ: Γ ⊢ ϕ ∴ Γ[σ] ⊢ ϕ[σ]
(si dans un contexte on sait une chose, alors si dans ce contexte on peut effectuer une certaine substitution, on sait qu’on peut faire cette substitution dans cette chose qu’on sait)

betaConv ((λv.t) u): ∴ Γ ⊢ (λv.t) u = t[u/v]
(l’application d’une fonction à un argument, est égale aux corps de cette fonction, dans lequel on a substitué le nom du paramètre de cette fonction, par l’expression sur laquelle on l’applique)

defineConst c t: ∴ ⊢ c = t
(définition d’une constante liée à une valeur)

defineTypeOp n abs rep vs: ⊢ ϕ t ∴ ⊢ abs (rep a) = a, ⊢ ϕ r = (abs (rep r) = r)


Notes

Le symbole « ∴ », représente le séquent, comme expliqué dans le message Re: Les logiques : notes en vrac, du 27 Avril 2014.

L’égalité ici, doit sûrement se comprendre comme une égalité syntaxique (pas l’unification), parce que sinon la règle “absThm v” n’aurait pas de sens. Il y a probablement d’autres choses implicites encore.

La règle “betaConv”, c’est la règle nommé β‑réduction dans le lambda‑calcul ; elle est parfois écrite “(λv.t) u = t[v := u]”, … une autre notation pour dire la substitution d’une liée, à une expression. D’ailleurs il faudra que j’en fasse un sujet, des règles du lambda‑calcul.

En plus de ces règles d’inférences, OpenTheory applique deux autres opérations : le renommage des types et des contextes pour éviter les conflits de noms dans certains contextes (ce qui rappel qu’on parle bien d’égalité syntaxique) et la composition de plusieurs théories en satisfaisant les suppositions (les prémisses) de l’une avec les théorèmes des autres.

Ce standard inclus quelques théories de base, auxquelles il est possible de se référer pour ne pas avoir à les répéter à chaque fois dans chaque fichier d’une théorie. Des théories sont incluses pour les choses suivantes :

  • Le type booléen;
  • les listes;
  • le type option;
  • les types produits (paires);
  • les types sommes (alternatives);
  • le type unité (unit);
  • les fonctions en général;
  • les entiers naturels;
  • les relations (c’est vague, pour moi).

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 : 15514
Mar 29 Déc 2015 04:28
Message Re: Les logiques : notes en vrac
Ajouté à la bibliographie de la page 2 : From LCF to HOL — a short history (cl.cam.ac.uk) [PDF], Mike Gordon, 2000.

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 : 15514
Ven 1 Jan 2016 03:36
Message Re: Les logiques : notes en vrac
Dans HOL4 (hol-theorem-prover.org), un assistant de démonstration, on dispose de huit primitives pour créer des théorèmes dérivés et donc des preuves :

  • ASSUME (introduction d’une supposition);
  • REFL (réflexivité);
  • BETA_CONV (béta‑conversion);
  • SUBST (substitution);
  • ABS (abstraction);
  • INST_TYPE (instanciation d’un type);
  • DISCH (décharge de supposition);
  • MP (modus‑ponem).

On peut reconnaitre des similitudes avec les dix règles d’inférence de HOL‑Light et les dix règles d’inférence de OpenTheory, tout en notant qu’il n’y en a ici que huit, au lieu de dix.

Je commenterai plus, plus tard, en ajoutant seulement pour le moment que quatre de ces huit règles, sont considérées comme des axiomes du système de déduction, et ces quatre axiomes, sont en fait eux‑mêmes une généralisation d’une logique de base.

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 : 15514
Jeu 19 Mai 2016 02:39
Message Re: Les logiques : notes en vrac
C’est dans l’œuvre d’Euclide, « Éléments », que semble avoir été posée pour la première fois à l’écrit, la méthode déductive appliquées aux mathématiques, environ 300 ans avant J.C..

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 : 15514
Jeu 15 Déc 2016 23:28
Message Re: Les logiques : notes en vrac
Les trois principaux systèmes d’axiomes en dehors de l’informatique, sont :

  • Les axiomes d’Euclide, pour la géométrie plane.
  • Les axiomes de Peano, pour les nombres entiers.
  • Les axiomes ZFC, Zermelo‑Fraenkel plus le théorème du choix, pour les mathématiques en général.

Notez qu’il est précisé « en dehors de l’informatique », ce qui explique que HOL n’y figure pas, alors qu’il en est souvent question dans ce sujet.

Ci‑dessous, une présentation du théorème de Gödel, orale et en images. C’est de cette présentation qu’est tirée cette liste de systèmes d’axiomes.

Les théorèmes d'incomplétude de Gödel — Science Étonnante № 37

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 : 15514
Sam 17 Déc 2016 22:26
Message Re: Les logiques : notes en vrac
Sur une interprétation et une démonstration en termes informatiques, du théorème d’incomplétude de Gödel.

Incomplétude — Passe‑Science № 7

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 : 15514
Dim 18 Déc 2016 10:38
Message Re: Les logiques : notes en vrac
Une présentation de Microsoft, dont les premières vignettes donnent en termes simples, un aperçu du fonctionnement des solveurs SMT : Satisfiability Modulo Theories: an appetizer (microsoft.com) [PDF], Leonardo de Moura, 2009.

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 : 15514
Ven 13 Jan 2017 21:49
Message Re: Les logiques : notes en vrac
Pour une anecdote, voir le sujet « Le mot “rationalisme” ».

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 : 15514
Dim 5 Mar 2017 01:38
Message Re: Les logiques : notes en vrac
À propos de quelques formes d’implication et de conséquence,
en logique : Réponse à “Implies vs. Entails vs. Provable” (math.stackexchange.com).

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 : 15514
Sam 15 Juil 2017 02:20
Message Re: Les logiques : notes en vrac
La logique et le « bon sens » ne sont pas la même chose. La logique ne fait pas partie du « bon sens » et le « bon sens » n’est pas toujours logique.

Un rappel tiré de cette vidéo, dont on peut conclure qu’il faut toujours interpréter une logique comme elle a été conçue, sans le faire dans un autre langage confondant logique et méta‑logique, et sans y incorporer des éléments d’une autre logique sans que ce ne soit prévu.

Quatre paradoxes de la logique mathématique — Science4All — 2016

Image
Hibou57

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