A Tactic Language for Ergo
A new version of the Ergo theorem prover is under development. It uses a single tactic language, based on <em>Angel</em>, for tactic programming, user interface, and proof representation. This paper describes the language as it is used in each of these cases, and explains the details of...
| Main Authors: | , , |
|---|---|
| Format: | Conference item |
| Published: |
Springer−Verlag
1997
|