Theory meets efficiency : a new implementation for proof trees

Overview & Synopsis

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.