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
}