= Term valuation
{title2=$t^{\mathcal A}[s]$}
A <first-order structure> and an <assignment in a first-order structure>[assignment] determine the value of every <first-order term>[term] recursively: a <logical variable>[variable] has its assigned value, a <constant symbol>[constant] has its interpreted value, and a compound <function> <first-order term>[term] is evaluated by applying the interpreted <function> to the recursively evaluated arguments. This operation supplies the input values for the <satisfaction for a set structure>[satisfaction] clauses of <atomic formulas>.
Back to article page
