Abstract
We describe some features of the tactic language implemented in the theorem prover Ergo 5. This is a variant of the generic tactic language Angel. We have adapted the language by changing the semantics of its parallel composition operator, the operator by which different tactics are applied to different branches in a proof tree. The paper includes a denotational semantics for this operator, and a collection of derived tactics which use it, together with a collection of algebraic laws which they obey. Keywords Tactic, Tactical, Denotational Semantics, Algebraic Laws, Interactive theorem proving 1 Introduction Theorem-proving tools have traditionally used their implementation language as a tactic language in which users can write procedures to assist in the discovery of proofs. In the LCF family of tools, this language is ML, with certain tactic combinators (tacticals) pre-defined.