Definition
Interpretation (Satisfiability Modulo Theory)
Let
be a many-sorted signature. A -interpretation assigns:
- a non-empty carrier
to every sort ; - a value
to every variable of sort ; - a total function
to every function symbol ; - a relation
to every predicate symbol . Equality on each sort is interpreted as identity. These assignments extend recursively to values of terms and truth values
of formulas.