What do we Need?
Model Existence
- Consistency of axiomatizations, to avoid CAX [ATP process]
- Use as a yes/no subroutine in more complex reasoning [Steen], including ...
- Axiom selection [SRASS]
- Existence of bugs in verification, but frustrating [McCune]
Model finder has to be trusted
Explicit Models
- Identification of bugs in verification [Claessen]
- A solution to a problem encoded as a model finding problem [Claessen]
- Inspecting outcomes of student's experiments [Steen]
- Evaluating formulae wrt the model [Sutcliffe]
- Machine learning from models [~Barbosa]
- Improve model finders [~Barbosa]
Models can be verified
Properties of Explicit Interpretations
- Verifiable [Zhang]
- Comprehensible for manual inspection, e.g., Intel [Korovin]
- ^C-tolerable evaluation of formulae [Sutcliffe]
In the language of the input!