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]

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]

Useful Explicit Interpretations

• For the whole signature [Bromberger, Schwarz, Weidenbach]
• ^C-tolerable evaluation of formulae [Caferra, Leitsch, Peltier; Sutcliffe]
• Verifiable [Zhang]
• Comprehensible for applications, e.g., Intel [Korovin]