On Role Logic

Details On Role Logic On Role Logic

2004-08-05

arxiv.org/abs/cs/0408018v1

Computer Science

Programming Languages

20 pages. Our later SAS 2004 result builds on this work

Scientific paper

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.

Affiliated with

Also associated with

No associations

Rating

On Role Logic does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with On Role Logic, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and On Role Logic will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-500770