Previous: TR 91-20 Next: TR 91-24

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.

Full Paper: Compressed postscript Compressed DVI

BibTeX entry