Interpretation Formats

Herbrand Interpretations

• Set of TPTP formulae
• Sample Herbrand Model
  • 
• Saturations are a special case
  • Guarantees the existence of a Herbrand model, not uniquely
  • Interpreting formulae might be difficult, inefficient, impossible!
  • Sample Saturation

Finite Interpretations

• Domain of distinct elements
• Total interpretation of functors and predicates
• Sample Finite Model

Integer and Real Interpretations

• $int and $real as domains
• Sample Integer Model
• Sample Real Model

Multiple Interpretations

• Uninterpreted functor is interpreted as each domain element
• Uninterpreted predicate is interpreted as $true and $false