16.1.5 Dominance Constraints

The syntax of our dominance logic DL is as follows:

$\begin{array}{rcl} \phi &::=& \phi \wedge \phi' \hmid X \dom Y \\ & & \hmid X\Neq f(X_1,\ldots,X_n) \\ & & \hmid \lambda(x)=y \end{array}$

where X_i, Y are variables and f is an atomic symbol from a given signature.

As for the semantics, a solution to a formula Phi consists of a finite tree T, a dominates relation, a lambda relation and an interpretation function I that maps each variable in Phi to a node in T. Further:

$x \dom y$ means that in the solution tree T, dominates .
$x\Neq f(x1 ... xn)$ means that is labeled by and has the nodes $I(x_1),\ldots,I(x_n)$ as immediate daughters (in that order).
$\lambda(x)=y$ means that is variable which is bound by the lambda node .