search

jrclogic / SMCDEL

A symbolic model checker for Dynamic Epistemic Logic.
https://w4eg.de/malvin/illc/smcdelweb
GNU General Public License v2.0
39 stars 9 forks source link

distributed knowledge #24

Closed m4lvin closed 4 months ago

m4lvin commented 1 year ago

Distributed knowledge is currently not expressible.

  1. A D :: [Agent] -> Form -> Form operator to say "It is distributed knowledge among ... that ..." should be added in SMCDEL.Language and the lexer and parser.

  2. Semantics for it need to be defined in at least the four main modules:

    • [ ] Explicit.S5
    • [ ] Explicit.K
    • [ ] Symbolic.S5
    • [ ] Symbolic.K

Side note: a more radical alternative might be to move completely to a PDL-style structure of epistemic modalities as done in "Logics of communication and change" https://doi.org/10.1016/j.ic.2006.04.006

foxyseta commented 6 months ago

Hi! Should the development branch be based on master or next?

m4lvin commented 6 months ago

Thanks for asking. Indeed it is better if you work on top of the next branch.

m4lvin commented 4 months ago

Done since https://github.com/jrclogic/SMCDEL/pull/36