Signature (Satisfiability Modulo Theory)

Definition

Signature (Satisfiability Modulo Theory)

An SMT signature is a many-sorted first-order vocabulary

$$\Sigma =(\mathcal{S},\mathcal{F},\mathcal{P}),$$

where:

• $\mathcal{S}$ is a set of sorts;
• every function symbol $f\in \mathcal{F}$ has a profile
  $f:s_1\times \cdots \times s_n\to s$, with $s_i,s\in \mathcal{S}$;
• every predicate symbol $P\in \mathcal{P}$ has a profile
  $P:s_1\times \cdots \times s_n\to \mathsf{Bool}$.

A function symbol with $n=0$ is a constant. The signature determines which
terms and formulas are well-sorted; it does not by itself impose arithmetic, array, or other theory laws. Those laws belong to the theory interpreted over the signature. For example, an integer-arithmetic signature may contain the sort $\mathsf{Int}$, constants such as $0$, and functions such as $+$, while the arithmetic theory specifies their intended meanings and properties.