DKAL and Z3: A Logic Embedding Experiment

Yuri Gurevich and Itay Neeman proposed the Distributed Knowledge Authorization Language, DKAL, as an expressive, yet very succinctly expressible logic for distributed authorization. DKAL uses a combination of modal and intuitionistic propositional logic. Modalities are used for qualifying assertions made by different principals and intuitionistic logic captures very elegantly assertions about basic information. Furthermore, a non-trivial and useful fragment known as the primal infon logic is amenable to efficient linear-time saturation. In this paper we experiment with an embedding of the full DKAL logic into the state-of-the-art Satisfiability Modulo Theories solver Z3 codeveloped by the second author. Z3 supports classical first-order semantics of formulas, so it is not possible to directly embed DKAL into Z3. We therefore use an indirect encoding. The one experimented with in this paper uses the instantiation-based support for quantifiers in Z3. Z3 offers the feature to return a pot...

• Type: Conference
• Year: 2010
• Where: BIRTHDAY
• Authors: Sergio Mera, Nikolaj Bjørner
• Keywords: Applied Computing, BIRTHDAY 2010, Intuitionistic Logic Captures, Intuitionistic Propositional Logic, Primal Infon Logic