Nous présentons dans ses grandes lignes un modèle de structuration de documents pour la génération automatique de preuves mathématiques. Le modèle prend en entrée des sorties d’un prouveur automatique et vise à produire des textes dont le style s’approche le plus possible des démonstrations rédigées par des humains. Cela implique la mise au point d’une stratégie de planification de document capable de s’écarter de la structure purement logique de la preuve. La solution que nous proposons consiste à intégrer de manière simple des informations de type intentionnel afin d’enrichir la structure rhétorique finale du texte.

Partant du principe que certaines phrases peuvent réaliser plusieurs actes de langage, i.e., dans une interface sémantique–pragmatique, plusieurs constituants de discours séparés, nous proposons, dans le cadre de la SDRT, un algorithme de construction de représentations sémantiques qui prend en compte tous les aspects discursifs dès que possible et de façon compositionnelle.