Rechercher

[Dem12] Vers un calcul des constructions pédagogique

Mémoire de Thèse : Soutenue le: 07 December 2012, pp. 139, pp.: Directeur: Patrick Cégielski
Rapporteur 1: Gilles Dowek
Rapporteur 2: Tristan Crolard
Membre du jury: Jean-Yves Marion
Membre du jury: Loïc Colson
Membre du jury: Sorin Stratulat, : Vers un calcul des constructions pédagogique,

Auteurs: V. Demange

motcle:
Résumé: Les systèmes pédagogiques sont apparus récemment à propos des calculs propositionnels (jusqu'à l'ordre supérieur), et consistent à donner systématiquement des exemples des notions (hypothèses) introduites. Formellement, cela revient à contraindre la règle d'hypothèse (Hyp) en déduction naturelle en une règle (P-Hyp) nécessitant la donnée d'exemples (i.e. instances prouvées) de formules introduites dans l'environnement. Autrement dit pour mettre un ensemble G de formules en hypothèse, il est requis de donner une substitution s telle que l'instance s(G) soit démontrable. Cette nécessité d'exemplification ayant été pointée du doigt par Poincaré (1913) comme relevant du bon sens: une définition d'un objet par postulat n'ayant d'intérêt que si un tel objet existe. Cette restriction appliquée à des systèmes formels intuitionnistes rejoint l'idée des mathématiques sans négation défendues par Griss (1946) au milieu du siècle dernier, et présentées comme une version radicale de l'intuitionnisme. À travers l'isomorphisme de Curry-Howard (1980), la contrepartie calculatoire est l'utilité des programmes définis dans les systèmes fonctionnels correspondant: toute fonction peut être appliquée à un argument clos. Les premiers résultats concernant les calculs propositionnels jusqu'au second ordre ont été publiés récemment par Colson et Michel (2007, 2008, 2009). Nous exposons dans ce rapport une tentative d'uniformisation et d'extension au Calcul des Constructions (CC) des précédents résultats. Tout d'abord une définition formelle et précise de sous-système pédagogique du Calcul des Constructions est introduite, puis différents tels sous-systèmes sont déclinés en exemple.

Download

BibTeX

@phdthesis {
Dem12,
title="{Vers un calcul des constructions pédagogique}",
author="V. Demange",
year=2012,
pages="139",
address="{CEDRIC Laboratory, Paris, France}",
note="{
Directeur: Patrick Cégielski
Rapporteur 1: Gilles Dowek
Rapporteur 2: Tristan Crolard
Membre du jury: Jean-Yves Marion
Membre du jury: Loïc Colson
Membre du jury: Sorin Stratulat}",
}