Conclusion

This Work

• Describes a (new) TPTP format for interpretations
• Describes a method and tool for verifying models
• Describes a tool for visualizing interpretations

Forthcoming Attractions

• Kripke interpretations for non-classical logic (done!)
• AGMV verification of Kripke interpretations (done!)
• Automated IIV for infinite interpretations (not done!)