A tactic-driven system for building proofs

Laurent Hascoet INRIA, BP93, 06902 Sophia-Antipolis, France

Proceedings of the 7th seminaire Programmation en Logique, Tregastel, France, 1988 (in French) (24 pages)

Abstract: We present a system to ease the process of building proof trees, which may be driven either manually by the user or automatically by user-defined tactics. Applications include: testing various strategies of resolution, partial evaluation of programs written with inference rules, building a theorem prover that automates structural induction strategies. We describe how to use the system for these applications. We examine the technical implementation considerations, as well as provide a brief user's manual.

Keywords: Natural semantics, static semantics, dynamic semantics, programming environments, proofs, inference rules, theorem proving, partial evaluation

Full text (in French) (pdf)


@inproceedings{Hascoet88b,
  author = {Hasco\"et, L.},
  title = {A tactic-driven system for building proofs},
  booktitle = {Proceedings of the 7th seminaire Programmation en Logique, Tregastel, France},
  note = {also Rapport de recherche \#0770, INRIA},
  url = "http://www.inria.fr/rrrt/rr-0770.html",  
  year = 1988
}