DKAL and Z3: A Logic Embedding Experiment

9 years 10 months ago
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...
Sergio Mera, Nikolaj Bjørner
Added 08 Nov 2010
Updated 08 Nov 2010
Type Conference
Year 2010
Authors Sergio Mera, Nikolaj Bjørner
Comments (0)