The TPTP Format for Interpretations

The TPTP World

Interpretations and Models

• What do we Need?
• What do we Have?

Tarskian Interpretations

• In One TF0 Formula
• In One TF0 File
• With Infinite Domains

Kripke Interpretations

• In One TX0 File
• With Infinite Domains and Worlds

Tools for Interpretations

• The AGMV Model Verifier
• The IIV Interactive Interpretation Viewer

Conclusion