Interactive and automated proof construction in type theory

Abstract

Type theory provides a homogeneous theoretical framework in which the construction of a function and the construction of a proof can be considered to be essentially the same activity. There is, however, a practical difference in that the development of a function requires more insight and therefore usually has to be performed under human guidance, whereas proof search can, to a large extent, be automated. Internally, Typelab exploits the homogeneity provided by type theory, while externally offering an interface to the human user which conceals most of the complexities of type theory. Interactive construction of proof objects is possible whenever desired; metavariables serve as placeholders which can be refined incrementally until the desired object is complete. For procedures which can reasonably be automated, high-level tactics are available. In this respect, Typelab can be understood as a proof assistant which, in addition to the manipulations of formulae traditionally performed by theorem provers, permits to carry out operations on entities such as functions and types.

For an illustration of program development in Typelab, the report TR-98-03 should be consulted, which holds an extended version of this chapter.

@Book{Deduction:98,
  author = 	 {W. Bibel and P. Schmitt},
  title = 	 {Automated Deduction --- A Basis for Applications},
  publisher = 	 {Kluwer Academic Publishers},
  year = 	 {1998}
}
@InCollection{Strecker:98a,
  author = 	 {M. Strecker and M. Luther and F. von Henke},
  title = 	 {{Interactive and automated proof construction in type theory}},
  booktitle =    "Automated Deduction --- A Basis for Applications",
  crossref =	 {Deduction:98},
  publisher =	 {Kluwer Academic Publishers},
  year =	 1998,
  editor =	 {W. Bibel and P. Schmitt}
  volume =	 {I: Foundations},
  chapter =	 {3: Interactive Theorem Proving}
}