| Auteur | Message |
|---|---|
|
Administrateur
 |
J’ajoute à la liste, « appréciation théorique vs appréciation pratique » ; l’appréciation devant se comprendre comme l’appréciation des qualités d’un système de déduction, langage logique, etc. Je dis « appréciation » au lieu de « jugement », pour ne pas créer une confusion (la notion de jugement étant une notion du domaine, qui a déjà sa définition).
|
|
|
|
Administrateur
|
Liens / « bibliographie »Ce message, dédié aux liens, sera mis à jour périodiquement. Les liens, assez sélectifs, ne seront pas résumés (c’est à prendre comme ça ou à laisser  ). C’est une sorte de bibliographie du sujet.
|
|
|
|
|
Administrateur
|
J’ajoute à la liste du premier message, « logique faible vs logique forte », même si je ne situe pas trop à quoi s’applique cet adjectif dans ce contexte : la sémantique, les axiomes, les règles, autre ? En fait, je le vois fréquemment en Anglais sous dans phrases du style “this logic is weak” ou “this logic is strong” et je ne sais même pas si la traduction correcte en français et bien « faible » et « forte ».
|
|
|
|
|
Administrateur
|
J’ajoute à la liste du premier message, « avantages supposés de FOL vs inconvénients supposés de HOL ». Je souligne bien « supposés », parce que ça me semble être plus de l’ordre du débat historique, éventuellement un peu pratique, plus que du débat théorique ou suffisamment pratique. Cette question semble exister cependant, et ce n’est pas moi qui décide de l’état des choses.
|
|
|
|
|
Administrateur
|
Je l’ai ajouté à la liste du message approprié, mais je le répète, parce qu’il est une justification de ce topic, qui comme il ne le dit pas explicitement, a un penchant pour les vérifications informatiques des preuves, comme il est possible de le constater en consultant le sélection de liens du message intitulé « Liens ».
How to really trust a mathematical proof (sciencenews.org). Julie Rehmeyer. Novembre 2008. Ça explique que les mathématiques utilisant des méthodes classiques, je veux dire, celles dont les preuves sont vérifiées par des humains, ne sont pas si exactes que ça, et qu’il y a toujours des doutes. On y apprend qu’il existe des preuves qui sont reconnues par certain(e)s mathématicien(ne)s et pas par d’autres et que la raison est les doutes pesant sur ces preuves. L’article prédit que l’avenir des mathématiques, est dans la vérification informatique des preuves. J’ajouterais que l’avenir de l’informatique (ou je l’espère), est réciproquement, dans les preuves mathématiques. |
|
|
|
|
Administrateur
|
La question « la logique dérive‑t‑elle des maths ou les maths dérivent‑elles de la logique ? », est assez parallèle à celle de comparer mathématiques et informatique, en se demandant laquelle dérive de l’autre.
À ce sujet, une citation, en réponse à la question “Is computer science a branch of mathematics?” : Citation : It is not uncommon to hear ideas along the lines that Source de la citation : Is computer science a branch of mathematics? — Réponse de ZYX (math.stackexchange.com). 24 Janvier 2014. |
|
|
|
|
Administrateur
|
First-Order Predicate Logic (rbjones.com) (également ajouté au message « Liens »), présente une application de SML pour la vérification de preuves dans la logique classique du premier ordre. C’est une approche des preuves assistées par l’informatique, dans la ligne de LCF, comme l’auteur (Roger Bishop Jones) le suggère lui‑même à la fin de son article.
Je rapporte une partie du résumé de présentation et la traduit juste en dessous. R. B. Jones a écrit : The system is a classical first-order predicate logic with two propositional connectives (not and implies) and a universal quantifier, presented as a "Hilbert style" axiom system in which there are two inference rules, modus ponens and generalisation, and six axiom schemata. Traduction a écrit : C’est un système de prédicats du premier ordre de la logique classique avec deux connecteurs propositionnels (négation et implication) et un quantificateur universel, présenté comme un système d’axiomes « à la Hilbert » comprenant deux règles d’inférence, modus‑ponem et généralisation, et six schémas d’axiomes. L’article présente une formulation en SML, concise. |
|
|
|
|
Administrateur
|
Au message listant des liens, est ajouté celui‑ci : Theory Management (cam.xrchz.net).
Ce n’est pas à propos de la théorie. Il répertorie succinctement quelques repères techniques (et donc pratiques) utiles, comme les formats d’échanges et transmission des théories (à ce sujet, voir aussi « Standard pour la transmission de preuves et théories ») et les prouveurs les plus répandus. |
|
|
|
|
Administrateur
|
J’ajoute à la liste du premier message, « sémantique axiomatique vs sémantique dénotationnelle vs sémantique opérationnelle ».
|
|
|
|
|
Administrateur
|
J’ajoute à la liste du premier message, « calcul des séquents vs déduction naturelle ».
|
|
|
|
