Portail:Logique/Archives Lumière sur
Quelques suggestion du 27 juin 2006[modifier le code]
Comme article je proposerais
- soit quelque chose sur les rapports entre intelligence artificielle et logique
- soit un article sur une logique non standard comme la logique déontique ou la logique de l´action.
Apierrot 27 juin 2006 à 20:47 (CEST)
Archives[modifier le code]
Du 27 juin au 27 juillet[modifier le code]
Frege renouvela de façon profonde la logique traditionnelle en développant le calcul des prédicats et le calcul des propositions modernes. Rêvant d´une refondation axiomatique des mathématiques, son projet sembla s´écrouler quand il apprit par Russell que son système axiomatique amenait à des paradoxes insurmontables : le fameux paradoxe des classes.
Du 27 juillet au XX[modifier le code]
De science abstraite et réservée aux élucubrations en chambre, la logique est devenue une véritable science expérimentale avec l'arrivée des assistants de preuves. L'un des plus utilisés est Coq. Il a permis de démontrer formellement et de faire vérifier mécaniquement par un ordinateur une démonstration du célèbre théorème des quatre couleurs. En Coq ont été démontrés et vérifiés mécaniquement des résultats de logique, comme la correction de Coq lui-même, plus précisément, de l'algorithme qui vérifie que les démonstrations de COQ sont correctes.
Si vous avez une nouvelle logique en tête et que vous voulez voir comment elle fonctionne. N'hésitez pas! Testez-là en Coq! En effet, Coq qui est fondé sur une logique constructive d'ordre supérieur pourra très probablement la «digérer».
Quelques suggestions du 6 octobre 2017[modifier le code]
- Parler d'induction ou récurrence et de coinduction.
- Parler de la forte normalisation et de la bonne fondation.
- Parler du lambda-calcul.
Pierre de Lyon (discuter) 6 octobre 2017 à 16:08 (CEST)