Combining Automated and Interactive Theorem Proving in Agda

Anton Setzer

(Swansea)

(Joint work with Karim Kanso)

We give an introduction into the theorem prover Agda. Then we show how to integrate automated theorem proving into the interactive theorem prover Agda. This is done by introducing a check function for a certain class of formulas in Agda and showing that this function returns true iff the corresponding formula holds. This way one can prove all true formulas of this class of formulas by applying this correctness proof to the trivial proof that the check function returns true. The check function will be defined in such a way that it is as simple as possible and that the correctness proof is simple. Now this check function is replaced by a builtin check function, which calls an automated theorem proving tool. We now obtain that if the automated theorem proving tool returns true, then we obtain a proof of the corresponding formula in Agda, which can be used for carrying out further proofs in Agda.

We illustrate this technique in case of a simple SAT solver.
Thursday 20th May 2010, 14:00
Video Conferencing Room - Far-134
Department of Computer Science