Extraction de Preuve

L'analyse systématique de preuves formelles visant à faire émerger des bornes quantitatives cachées, des algorithmes constructifs, un contenu computationnel ou des données effectives implicitement encodées par des dérivations non constructives ou de haut niveau.