Accueil Dernière Parution Auteurs Thèmes Mots-clefs Parutions Videos Recherche guidée Comité de lecture Contact Abonnement Soumission d'article   Version anglaise Collection numérisée également sur NUMDAM pour les n°1 à n°148 et sur Revues.org pour les n° 149 et suivants

Recherche selon le critère: Thème: Calcul Affiner ou élargir la recherche Résultats n° 1 à 8 sur un total de 20 entrées référencées Page 1 . 2 . 3 . >> Page suivante Titre La théorie des types et les systèmes informatiques de traitement de démonstrations mathématiques Auteur DOWEK Gilles Mots-clefs Calcul, Démonstration, Fonction, Langage mathématique, Raisonnement, Systèmes de traitement de démonstrations mathématiques, Théorie des ensembles, Théorie des types Thèmes Calcul, Ensembles (Théorie des), Informatique, Logiciel, Logique Résumé Depuis la fin des années soixante, on a vu apparaître plusieurs logiciels destinés à traiter des connaissances mathématiques, en particulier des démonstrations formelles. La réalisation de tels logiciels pose de nouveaux problèmes, en particulier celui de la conception de cadres logiques dans lesquels les mathématiques puissent être formalisées en fait. Cela renouvelle la problématique des fondements des mathématiques, jusque-là davantage concentrée sur la potentialité de la formalisation que sur son actualité. Plusieurs raisons expliquent que les concepteurs de tels logiciels choisissent bien souvent de formaliser les mathématiques en théorie des types, plutôt qu'en théorie des ensembles. Numéro 165, Printemps 2004, n° spécial La théorie constructive des types Langue   Français Lire l'article Titre Sémantique computationnelle dans la théorie des types Auteur RANTA Aarne Mots-clefs Grammaire de Montague, Sémantique logique, Théorie des types Thèmes Arbres, Calcul, Linguistique, Logique, Sémantique, Types (Théorie des) Résumé Cet article montre une formalisation complète des grammaires à la Montague dans le cadre de GF (Grammatical Framework), une formalisation qui est en même temps une implémentation déclarative. Cette implémentation comprend toutes les opérations fondamentales du modèles PTQ de Montague : la construction des arbres d'analyse, la linéarisation des arbres en chaînes de caractères, et l'interprétation des arbres comme formules logiques. De plus, un algorithme d'analyse syntaxique est dérivé de toute grammaire représentée dans GF. Comme GF est une théorie constructive des types avec des types dépendants, la technique utilisée pour les grammaires classiques de Montague est généralisée au cas où l'isomorphisme de Curry-Howard est utilisé pour expliquer la référence anaphorique. D'autre part, GF impose une condition de compositionnalité qui est plus forte que celle du PTQ. Ceci empêche la formulation des règles dites "quantifying in" de Montague. Nous arrivons ainsi à des formulations alternatives de ces règles utilisant des combinateurs et des constituants discontinues. Le fragment PTQ est aussi présenté comme exemple de la modification d'une grammaire GF par remplacement de l'anglais par une autre langue de cible, le français. L'article conclut par une discussion sur les rôles complémentaires d'une syntaxe logique et d'une syntaxe linguistique. Numéro 165, Printemps 2004, n° spécial La théorie constructive des types Langue  Anglais Lire l'article Titre Charles Babbage (1791-1871) : de l'Ècole Algébrique Anglaise à la "machine analytique" Auteur DURAND-RICHARD Marie-Josée Mots-clefs Aucun Thèmes Algèbre, Analyse mathématique, Calcul, Histoire des mathématiques, Histoire des sciences, Informatique Résumé Numéro 118, Été 1992 Langue   Français Document non disponible Titre Groupe inter-IREM d'épistémologie, "La rigueur et le calcul. Documents historiques et épistémologiques", Paris, CEDIC, 1982 Auteur BRESSON Denis Mots-clefs Aucun Thèmes Analyse bibliographique, Calcul, Epistémologie, Histoire des mathématiques Résumé Analyse bibliographique Numéro 83, Automne 1983 Langue   Français Document non disponible Titre N. F. Stewart, F. Jensen, "Solutions numériques des problèmes matriciels", Montréal, Les Presses de l'Université de Montréal, Paris, Eyrolles, 1975 Auteur BRESSON Denis Mots-clefs Aucun Thèmes Analyse bibliographique, Calcul, Linéaire (Algèbre) Résumé Analyse bibliographique Numéro 55, Automne 1976 Langue   Français Document non disponible Titre B. Demidovitch, I. Maron, "Eléments de Calcul numérique", Moscou, Editions Mir, 1973 Auteur BRESSON Denis Mots-clefs Aucun Thèmes Analyse bibliographique, Calcul, Linéaire (Algèbre) Résumé Analyse bibliographique Numéro 55, Automne 1976 Langue   Français Document non disponible Titre N. Bakhvalov, "Méthodes numériques", Moscou, Editions Mir, 1976 Auteur BRESSON Denis Mots-clefs Aucun Thèmes Analyse bibliographique, Calcul, Linéaire (Algèbre) Résumé Analyse bibliographique Numéro 55, Automne 1976 Langue   Français Document non disponible Titre Modèles pour la traduction automatique Auteur VAUQUOIS Bernard Mots-clefs Aucun Thèmes Calcul, Informatique, Linguistique Résumé Numéro 34, Été 1971, n° spécial Quelques aspects de la formalisation en linguistique - 1 Langue   Français Lire l'article Page 1 . 2 . 3 . >> Page suivante Droits des utilisateurs : Cette création est mise à disposition sous un contrat Creative Commons