Higher Order Proof Engineering: Proof Collaboration, Transformation, Checking and Retrieval

Shuai Wang 1, *
* Auteur correspondant
Abstract : Higher Order Logic has been used in formal mathematics, software verification and hardware verification over the past decades. Recent developments of interactive theorem made sharing proofs between some theorem provers possible. This paper first gives an introduction and an overview of related recent advances, followed by the proof checking benchmarks of a proof sharing repository, namely OpenTheory (after proof transformation by the upgraded Holide). Finally, we introduce ProofCloud, the first proof retrieval engine for higher order proofs.
Type de document :
Communication dans un congrès
AITP 2016 - Conference on Artificial Intelligence and Theorem Proving, Apr 2016, Obergurgl, Austria
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01250197
Contributeur : Shuai Wang <>
Soumis le : lundi 4 janvier 2016 - 14:21:28
Dernière modification le : mardi 9 janvier 2018 - 14:13:26

Fichier

aitp_2016_final.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01250197, version 1

Collections

Citation

Shuai Wang. Higher Order Proof Engineering: Proof Collaboration, Transformation, Checking and Retrieval. AITP 2016 - Conference on Artificial Intelligence and Theorem Proving, Apr 2016, Obergurgl, Austria. 〈hal-01250197〉

Partager

Métriques

Consultations de la notice

157

Téléchargements de fichiers

171