Vers un démonstrateur adaptatif

Dans le traitement informatique de la preuve, trois courants principaux sont distingués, – à tendance formelle, – à tendance cognitive, – à tendance pragmatique. – 1. Introduction; – 2. Construire un démonstrateur adaptatif : un catalogue de problèmes; – 3. Le système de déduction (Le calcul des propositions; Un calcul de séquent); – 4. Généralisation à partir d’exemples; – 5. Généralisation de formules : les macro-connecteurs (Formules à généraliser. Cas particulier : les formules homogènes; Langage des généralisations : les macro-connecteurs; Méthode de généralisation; En résumé); – 6. Généralisation des lemmes (Les concepts à apprendre; Langage des généralisations : les schémas sous contraintes; Propriétés des schémas sous contrainte; Mécanismes de généralisation; En résumé); – 7. Conclusion.