@TechReport{AIDA-91-21,
  author = 	"Thierry Boy de la Tour and Christoph Kreitz",
  title = 	"Building Proofs by Analogy Using NuPRL's Built-in Curry-Howard
	Isomorphism",
  institution = 	"FG Intellektik, FB Informatik, TH Darmstadt",
  year = 	"1991",
  OPTtype = 	"",
  number = 	"AIDA--91--21",
  OPTaddress = 	"",
  OPTmonth = 	"",
  note = 	"In A.~Voronkov, editor,
        {\em LPAR'92, Proceedings of the Conference on Logic Programming
        and Automated Reasoning, St.~Petersburgh, Russia, July 1992}
        Lecture Notes in Artifical Intelligence 624, pp.~202--213.
        Springer Verlag, 1992",
  abstract = "We present a formal method for building proofs by analogy and its implementation
as a proof tactic for the NuPRL proof development system. The
Curry-Howard Isomorphism is used to represent proof constructions in a
term-functional language and to specify analogies by transformation rules on
these terms.
The method has the advantage to admit {\em complete} formalization and to make
use of well-known techniques like higher-order unification."
}