A Calculus of Tactics and Its Operational Semantics
Gueorgui Jojgov, Herman Geuvers · Electronic Notes in Theoretical Computer Science · 2004
This paper presents work in progress on a calculus of tactics for a hypothetical interactive theorem prover based on a λ-calculus for higher-order logic (λHOL). The calculus of tactics is an extension of a calculus of open terms for λHOL. In contrast to other systems where the semantics of tactics is given by the semantics of their implementation in a general programming language (e.g. OCAML) we are able to define what a tactic does in terms of the state of the theorem prover expressed by an open term that encodes the incomplete proof created so far at that given state. We present typed operational semantics for the tactics calculus and show that it is sound and complete with respect to the calculus of open terms. The soundness theorem goes further to establish the relation between the states of the prover before and after the execution of a tactic.