Project Presentation: Algorithmic Structuring and Compression of Proofs (ASCOP)

Stefan Hetzl 1
1 PARSIFAL - Proof search and reasoning with logic specifications
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France
Abstract : Computer-generated proofs are typically analytic, i.e. they essentially consist only of formulas which are present in the theorem that is shown. In contrast, mathematical proofs written by humans almost never are: they are highly structured due to the use of lemmas. The ASCOP-project aims at developing algorithms and software which structure and abbreviate analytic proofs by computing useful lemmas. These algorithms will be based on recent groundbreaking results establishing a new connection between proof theory and formal language theory. This connection allows the application of e cient algorithms based on formal grammars to structure and compress proofs.
Type de document :
Communication dans un congrès
Conferences on Intelligent Computer Mathematics (CICM) 2012, Jul 2012, Bremen, Germany. 2012
Liste complète des métadonnées

Littérature citée [15 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-00776337
Contributeur : Stefan Hetzl <>
Soumis le : mardi 15 janvier 2013 - 13:58:05
Dernière modification le : mercredi 14 novembre 2018 - 16:14:01
Document(s) archivé(s) le : mardi 16 avril 2013 - 03:55:02

Fichier

ascop.pdf
Fichiers éditeurs autorisés sur une archive ouverte

Identifiants

  • HAL Id : hal-00776337, version 1

Collections

Citation

Stefan Hetzl. Project Presentation: Algorithmic Structuring and Compression of Proofs (ASCOP). Conferences on Intelligent Computer Mathematics (CICM) 2012, Jul 2012, Bremen, Germany. 2012. 〈hal-00776337〉

Partager

Métriques

Consultations de la notice

208

Téléchargements de fichiers

118