| We present role logic, a notation for describing properties
of relational structures in shape analysis, databases, and
knowledge bases. We construct role logic using the ideas of
de Bruijn's notation for lambda calculus, an encoding of
first-order logic in lambda calculus, and a simple rule for
implicit arguments of unary and binary predicates.
The unrestricted version of role logic has the expressive
power of first-order logic with transitive closure. Using a
syntactic restriction on role logic formulas, we identify a
natural fragment RL^2 of role logic. We show that the RL^2
fragment has the same expressive power as two-variable logic
with counting C^2 and is therefore decidable.
We present a translation of an imperative language into the
decidable fragment RL^2, which allows compositional
verification of programs that manipulate relational
structures. In addition, we show how RL^2 encodes boolean
shape analysis constraints and an expressive description
logic. |