Building proofs by Analogy via the Curry-Howard Isomorphism.

Thierry Boy de la Tour, Christoph Kreitz.

In A. Voronkov, ed., Conference on Logic Programming and Automated Reasoning (LPAR'92),
LNCS 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 complete formalization and to make use of well-known techniques like higher-order unification.


Also presented at the GWAI-92 Workshop "Kontrolle von Problemlöseverfahren", Bonn, Germany, September 1992.

Paper is available in
postscript and pdf format
  Slides of the conference presentation are available in compressed postscript and pdf format
(Presentation: Thierry Boy de la Tour)




Bibtex Entry


BACK
Back to overview of papers
@InProceedings{inp:BoyKreitz92a, author = "Thierry Boy~de~la~Tour and Christoph Kreitz", title = "Building Proofs by Analogy via the {Curry-Howard} Isomorphism", booktitle = "{LPAR'92}, Conference on Logic Programming and Automated Reasoning", year = "1992", editor = "A. Voronkov", pages = "202--213", series = Lecture Notes in Computer Science", volume = "624", publisher = "Springer Verlag" }