Auto in Agda - Programming Proof Search Using Reflection.
Pepijn Kokke, Wouter Swierstra · 2015
Abstract. As proofs in type theory become increasingly complex, there is a growing need to provide better proof automation. This paper shows how to implement a Prolog-style resolution procedure in the dependently typed programming language Agda. Connecting this resolution proce-dure to Agda’s reflection mechanism provides a first-class proof search tactic for first-order Agda terms. As a result, writing proof automation tactics need not be different from writing any other program. 1