smcdel alternatives and similar packages
Based on the "Logic" category.
Alternatively, view smcdel alternatives based on common mentions on social networks and blogs.
-
tamarin-prover
Main source code repository of the Tamarin prover for security protocol verification. -
atp-haskell
Haskell version of the code from "Handbook of Practical Logic and Automated Reasoning" -
logic-classes
Framework for propositional and first order logic, theorem proving -
structural-induction
SII: Structural Induction Instantiator over any strictly-positive algebraic data type. -
g4ip-prover
Theorem prover for intuitionistic propositional logic, fork of github.com/cacay/G4ip -
tpdb
parser and prettyprinter for TPDB syntax (termination problem data base) -
haskhol-core
The core logical system of the HaskHOL theorem prover. See haskhol.org for more details.
Clean code begins in your IDE with SonarLint
* Code Quality Rankings and insights are calculated and provided by Lumnify.
They vary from L1 to L5 with "L5" being the highest.
Do you think we are missing an alternative of smcdel or a related project?
README
SMCDEL
A symbolic model checker for Dynamic Epistemic Logic.
You can find a complete literate Haskell documentation in the file SMCDEL.pdf.
References
Malvin Gattinger: Towards Symbolic Factual Change in DEL. ESSLLI 2017 student session, 2017.
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 trystack build
again.stack install
will put two executablessmcdel
andsmcdel-web
into ~/.local/bin which should be in yourPATH
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](https://github.com/jrclogic/SMCDEL/tree/master/Examples).
4) To use the web interface run smcdel-web
and then open http://localhost:3000/index.html.
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.
- Data.HasCacBDD which runs CacBDD from http://kailesu.net/CacBDD/
- Cudd (with some patches)