Is it possible / meaningful to get UNSAT cores or models in a format that is meaningful in Lean?
We are representing domain models and some queries against those models. We would (if possible) like to get witnesses to proof failures expressed in a meaningful way back into Lean, and to get UNSAT cores that have meaning in Lean.
The underlying idea is that we want users to be able to "ask questions" about domain models by checking whether partially instantiated ground terms are conformant with the model and then presenting the results back in a meaningful way.
Mostly I am curious whether this is on your roadmap for any point in the future.
Is it possible / meaningful to get UNSAT cores or models in a format that is meaningful in Lean?
We are representing domain models and some queries against those models. We would (if possible) like to get witnesses to proof failures expressed in a meaningful way back into Lean, and to get UNSAT cores that have meaning in Lean.
The underlying idea is that we want users to be able to "ask questions" about domain models by checking whether partially instantiated ground terms are conformant with the model and then presenting the results back in a meaningful way.
Mostly I am curious whether this is on your roadmap for any point in the future.