Graceful movement toward theorem proving?

1

I’m working on realistic models of networking with industrial uses, and starting to formulate some useful, nontrivial theorems. Although the Analyzer finds no counterexamples to these theorems, the analyzable domains are not big enough to be convincing. I’ve already streamlined the model, and I don’t think optimizing it further is likely to be the answer. The answer is likely to be theorem-proving, but it would be nice to move from pure Alloy to theorem-proving in an incremental way. I know there are Alloy theorem-provers—which are mature? Has anyone done research on methods for this? Does anyone think there are interesting research questions in this area?

1 Like