May 29, 2017

> There ought to be some representation for theorem resolvers that is good for general purpose programming. It's just that nobody found it yet.

There are some nice examples of search-based programming in Z3 (using the Python API) in https://yurichev.com/writings/SAT_SMT_draft-EN.pdf , if that is along the lines of what you meant.