3 ms·
Now I am interested in what exactly your use case is :-) Maybe you would want to model this first in a general purpose interactive prover such as Isabelle, and
by auggierose 3y ago
Now I am interested in what exactly your use case is :-)
Maybe you would want to model this first in a general purpose interactive prover such as Isabelle, and proceed from there. But in the end you seem to be looking for a push-button algorithm for proving the consistency of a particular logic, and I can tell you, that's probably not gonna end well.
- PartiallyTyped 3y agoI can't say much more unfortunately, not yet at least. I have semi-sketched the idea in Dafny instead of Isabelle. Direct encoding of arrays makes it difficult, but I am thinking iterative deepening might just work. I am working on a Z3 approach for this, and I am crossing my fingers. If Z3 doesn't work, I will try emitting Dafny code instead and hooking up to the compiler.