Introduction

Model Finding is Useful

• An interpretation maps formulae to truth values
• A model of a formula maps it to true
• Disprove by finding a model of the axioms, not of the conjecture
• Such a countermodel can show why a conjecture is not a theorem
• Applications: verification, axiom checking, problem solving

Tarskian Interpretations

• A domain and mappings
• Map functions applied to domain elements to domain elements
• Map predicates applied to domain elements to truth values
• Evaluate (⊢) closed formulae
• Saturations are another (hardly useful) form

This Work

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