Theory meets efficiency : a new implementation for proof trees

Laurent Hascoet 1
1 CROAP - Design and Implementation of Programming Tools
CRISAM - Inria Sophia Antipolis - Méditerranée
Abstract : The implementation of a system for manipulating proof trees shows that the time spent on basic manipulations of proof trees and inference rules is critical, as well as the memory space used. This paper describes a new data structure, D-trees, to represent proof trees and inference rules. This structure is designed to optimize the time spent to find inference rules applicable to a subgoal of a proof, as well as applying such an inference rule to the proof tree. It is also designed to consume very small memory space. This implementation is very closely related to formulas as types theories, so that it becomes clearer to understand and easier to check.
Type de document :
[Research Report] RR-1109, INRIA. 1989
Liste complète des métadonnées
Contributeur : Rapport de Recherche Inria <>
Soumis le : mercredi 24 mai 2006 - 18:14:54
Dernière modification le : samedi 27 janvier 2018 - 01:31:04
Document(s) archivé(s) le : mardi 12 avril 2011 - 19:06:49



  • HAL Id : inria-00075450, version 1



Laurent Hascoet. Theory meets efficiency : a new implementation for proof trees. [Research Report] RR-1109, INRIA. 1989. 〈inria-00075450〉



Consultations de la notice


Téléchargements de fichiers