Interpreting wrt an Interpretation

Why

• Determine semantics of terms, atoms, formulae
• Used by semantically guided ATP systems and tools

What

• Formula/term and model input, semantic interpretation output
• Hopefully polynomial time (what does that mean?)
• Implemented as libraries, with support for persistent models

How

• Directly wrt finite interpretations
  • Evaluate ground terms/atoms in integer and real models
• Theorem proving with model as axioms, formula as conjecture
  • THM = true , CTH = false
  • If complete: SAT = true, CSA = false
  • Do in parallel