Combining Proofs to form Different Proofs

Abstract : Different Automated Theorem Proving (ATP) systems solve different parts of different problems in different ways. Given a set of proofs produced by ATP systems based on adequately common principles, it is possible to create new proofs by combining proof components extracted from the proofs in the set. It is not generally easy to say that one of the original or new proofs is better or worse than another, but ways to show that two proofs are different are available. This paper describes a process of proof combination to form new proofs that are different from the original set of proofs.
Type de document :
Communication dans un congrès
Pascal Fontaine and Aaron Stump. First International Workshop on Proof eXchange for Theorem Proving - PxTP 2011, Aug 2011, Wrocław, Poland. 2011
Liste complète des métadonnées

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

https://hal.inria.fr/hal-00677234
Contributeur : Pascal Fontaine <>
Soumis le : mercredi 7 mars 2012 - 15:48:20
Dernière modification le : mercredi 7 mars 2012 - 16:22:20
Document(s) archivé(s) le : vendredi 23 novembre 2012 - 16:01:14

Fichier

paper6.pdf
Accord explicite pour ce dépôt

Identifiants

  • HAL Id : hal-00677234, version 1

Collections

Citation

Geoff Sutcliffe, Cynthia Chang, Deborah Mcguinness, Tim Lebo, Li Ding, et al.. Combining Proofs to form Different Proofs. Pascal Fontaine and Aaron Stump. First International Workshop on Proof eXchange for Theorem Proving - PxTP 2011, Aug 2011, Wrocław, Poland. 2011. 〈hal-00677234〉

Partager

Métriques

Consultations de la notice

199

Téléchargements de fichiers

146