Popularity
7.1
Declining
Activity
5.6
Declining
18
4
2

Monthly Downloads: 26
Programming language: Haskell
License: GNU General Public License v2.0 only
Tags: Logic    
Latest version: v1.1.0

smcdel alternatives and similar packages

Based on the "Logic" category

Do you think we are missing an alternative of smcdel or a related project?

Add another 'Logic' Package

README

SMCDEL

Release Hackage Build Status DOI

A symbolic model checker for Dynamic Epistemic Logic.

You can find a complete literate Haskell documentation in the file SMCDEL.pdf.

References

Johan van Benthem, Jan van Eijck, Malvin Gattinger, and Kaile Su: Symbolic Model Checking for Dynamic Epistemic Logic. In: Proceedings of The Fifth International Conference on Logic, Rationality and Interaction (LORI-V), 2015.

Johan van Benthem, Jan van Eijck, Malvin Gattinger, and Kaile Su: Symbolic Model Checking for Dynamic Epistemic Logic --- S5 and Beyond. Journal of Logic and Computation, 2017.

Malvin Gattinger: Towards Symbolic Factual Change in DEL. ESSLLI 2017 student session, 2017.

Malvin Gattinger: New Directions in Model Checking Dynamic Epistemic Logic. PhD thesis, ILLC, Amsterdam, 2018.

Online

You can try SMCDEL online here: https://w4eg.de/malvin/illc/smcdelweb/

Dependencies

On Debian, just do sudo apt install graphviz dot2tex.

Basic usage

1) Use stack from https://www.stackage.org

  • stack build will compile everything. This might fail if one of the BDD packages written in C and C++ is missing. In this case, install those manually and then try stack build again.

  • stack install will put two executables smcdel and smcdel-web into ~/.local/bin which should be in your PATH variable.

2) Create a text file MuddyShort.smcdel.txt which describes the knowledge structure and the formulas you want to check for truth or validity:

```
-- Three Muddy Children in SMCDEL
VARS 1,2,3
LAW  Top
OBS  alice: 2,3
     bob:   1,3
     carol: 1,2
WHERE?
  [ ! (1|2|3) ] alice knows whether 1
VALID?
  [ ! (1|2|3) ]
  [ ! ((~ (alice knows whether 1)) & (~ (bob knows whether 2)) & (~ (carol knows whether 3))) ]
  [ ! ((~ (alice knows whether 1)) & (~ (bob knows whether 2)) & (~ (carol knows whether 3))) ]
  (alice,bob,carol) comknow that (1 & 2 & 3)
```

3) Run smcdel MuddyShort.smcdel.txt resulting in:

```
>> smcdel MuddyShort.smcdel.txt
SMCDEL 1.0 by Malvin Gattinger -- https://github.com/jrclogic/SMCDEL

At which states is ... true?
[]
[1]

Is ... valid on the given structure?
True
```

More example files are in the folder Examples.

Advanced usage

To deal with more complex models and formulas, use SMCDEL as a Haskell module.

Examples can be found in the folders src/SMCDEL/Examples and bench.

Used BDD packages

SMCDEL can be used with different BDD packages. To compile and run the benchmarks you will have to install all of them.