#
Theory meets efficiency: a new implementation for Proof Trees

*Laurent Hascoet*
*INRIA, BP93, 06902 Sophia-Antipolis, France*

INRIA Research Report #1109, october 1989 (16 pages)

**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.

**Keywords:**
Inference rules, Proof trees, Formulas as Types, Difference lists

Full text (pdf)
`
@techreport{Hascoet89,
author = {Hasco\"et, L.},
title = {Theory meets efficiency: a new implementation for Proof Trees},
institution = {INRIA},
type = {Research Report},
number=1109,
url = "http://www.inria.fr/rrrt/rr-1109.html",
year=1989
}
`