<< Prev | - Up - | Next >> |
The syntax of our dominance logic DL is as follows:
where 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:
means that in the solution tree T, dominates .
means that is labeled by and has the nodes as immediate daughters (in that order).
means that is variable which is bound by the lambda node .
<< Prev | - Up - | Next >> |