Proof checking
Tactic
A procedure that constructs or refines a proof.
Definition
Tactic
A tactic reads a proof state and tries to produce proof terms or smaller goals.
Tactics automate common reasoning patterns and search. In a kernel-based system, their output must still pass the kernel.
01
Example
An induction tactic can create a base goal and an inductive-step goal for a statement about natural numbers.
02
Important distinction
A tactic succeeding does not bypass the kernel unless the system explicitly trusts that tactic as an axiom or oracle.
After reading this article, you should be able to
- Define Tactic in the sense used on this site.
- Describe how tactic execution relates to the proof term checked by a kernel.