Proof Search in an Authorization Logic

摘要

We consider the problem of proof search in an expressive authorization logic that contains a 'says' modality and an ordering on principals. After a description of the proof system for the logic, we identify two fragments that admit complete goal-directed and saturating proof search strategies. A smaller fragment is then presented, which supports both goal- directed and saturating search, and has a sound and complete translation to first-order logic. We conclude with a brief description of our implementation of goal-directed search.