#
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
}
`