Interpretation (Satisfiability Modulo Theory)

Definition

Interpretation (Satisfiability Modulo Theory)

Let $\Sigma =(\mathcal{S},\mathcal{F},\mathcal{P})$ be a many-sorted signature. A $\Sigma$-interpretation $I$ assigns:

• a non-empty carrier $D_s^I$ to every sort $s\in \mathcal{S}$;
• a value $x^I\in D_s^I$ to every variable $x$ of sort $s$;
• a total function $$f^I:D_{s_1}^I\times \cdots \times D_{s_n}^I\to D_s^I$$ to every function symbol $f:s_1\times \cdots \times s_n\to s$;
• a relation $$P^I\subseteq D_{s_1}^I\times \cdots \times D_{s_n}^I$$ to every predicate symbol $P:s_1\times \cdots \times s_n\to \mathsf{Bool}$.

Equality on each sort is interpreted as identity. These assignments extend recursively to values of terms and truth values $I(\phi )\in \{0,1\}$ of formulas.