Three Tactic Theorem Proving

Explaination of the key features of the proof description language of DECLARE, an experimental theorem provider for high order logic. We take a somewhat radical approach to proof description: proofs are not described with tactics but by using three expressive outling constructs. We also assess the costs and benefits of this approach, and describe its impact on three areas of theorem prover design: specification, automated reasoning and interaction.