Sciweavers

CORR
2004
Springer

On Role Logic

13 years 3 months ago
On Role Logic
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 RL2 of role logic. We show that the RL2 fragment has the same expressive power as two-variable logic with counting C2 , and is therefore decidable. We present a translation of an imperative language into the decidable fragment RL2 , which allows compositional verification of programs that manipulate relational structures. In addition, we show how RL2 encodes boolean shape analysis constraints and an expressive description logic.
Viktor Kuncak, Martin C. Rinard
Added 17 Dec 2010
Updated 17 Dec 2010
Type Journal
Year 2004
Where CORR
Authors Viktor Kuncak, Martin C. Rinard
Comments (0)