Applying the Formal Decision Procedure

Let $d=extract(dp)\; (rep\,(H\vdash G))$. The value of d is either inl(p) for some proof p or inr(f) for some function f. In the case of inl(p), we have $p\in\exists p:{\sf PropProof}.root(p)=rep\,(H\vdash G)$. Notice that P=decide(d; u.u; v.v). Let $\hat{d}$ be the term decide(p; u.u; v.v).

We can now prove $H \vdash G$ by reflection if it is true.

$$H \vdash G$$

We can write a tactic

which checks d for inl(p), writes $\hat{d}$ and uses it as the witness, or fails.

$H \vdash G$ by Decide(dp).

This simple example illustrates the essential ideas behind the method of using relfection to justify decision procedures and for type checking in programming languages [10]. I think that this will be an important technique for modern provers that employ decision procedures. There are many other uses of reflection, and I recommend `looking at articles by Boyer and Moore [8], Weyrauch [50], Howe [29], as well as [3,6,16,37,47,48].