An Agda binding to an SMT solver

Potential supervisors: 

The purpose of this project is to connect an SMT solver to Agda. Agda is a proof assistant for an expressive logic, and SMT solvers are automated theorem provers for more restricted logics. The idea is to make it possible to leverage the automation of an SMT solver in Agda proofs.

However, the goal is not simply to ask an SMT solver whether a certain statement holds and then taking this statement at face value. The goal is to make use of the output of an SMT solver to construct proof terms in Agda's logic.

This kind of connection between an SMT solver and a proof assistant has already been developed for Coq, which is similar to Agda. Hopefully lessons and ideas from that project can be reused in this one. For information about that project, see

Contact: Nils Anders Danielsson

Date range: 
October, 2018 to October, 2023