Technical report: Intellektik 91-21
Building Proofs by Analogy Using NuPRL's Built-in Curry-Howard Isomorphism
Thierry Boy de la Tour and Christoph Kreitz
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 complete
formalization and to make
use of well-known techniques like higher-order unification.