paper ps
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.

### Citation

Viktor Kuncak and Martin Rinard.
On role logic.
Technical Report 925, MIT CSAIL, 2003.### BibTex Entry

@techreport{KuncakRinard03OnRoleLogic,
author = {Viktor Kuncak and Martin Rinard},
title = {On Role Logic},
institution = {MIT CSAIL},
number = 925,
year = 2003,
url = {http://arxiv.org/abs/cs.PL/0408018},
abstract = {
We present {\em 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.
}
}