Popularity

8.3

Growing

Activity

2.8

Stars 46

Watchers 7

Forks 9

Last Commit 3 months ago

Monthly Downloads: 4

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.
Alternatively, view smcdel alternatives based on common mentions on social networks and blogs.

tamarin-prover

9.8 8.4 smcdel VS tamarin-prover

Main source code repository of the Tamarin prover for security protocol verification.
hatt

7.7 0.0 smcdel VS hatt

Truth-table generator for classical propositional logic

InfluxDB – Built for High-Performance Time Series Workloads

InfluxDB 3 OSS is now GA. Transform, enrich, and act on time series data directly in the database. Automate critical tasks and eliminate the need to move data externally. Download now.

Promo www.influxdata.com

tip-haskell-frontend

7.5 2.1 smcdel VS tip-haskell-frontend

Convert from Haskell to Tip
hout

7.3 0.0 smcdel VS hout

A non-interactive proof assistant using the Haskell type system
atp-haskell

7.0 4.8 smcdel VS atp-haskell

Haskell version of the code from "Handbook of Practical Logic and Automated Reasoning"
picologic

6.6 0.0 smcdel VS picologic

Symbolic logic expressions
picosat

6.6 0.0 L2 smcdel VS picosat

Haskell bindings for PicoSAT solver
logic-classes

5.9 0.0 smcdel VS logic-classes

Framework for propositional and first order logic, theorem proving
jukebox

5.8 0.0 smcdel VS jukebox

A theorem prover
Heyting Algebras

5.7 0.0 smcdel VS Heyting Algebras

Heyting Algebras in Haskell
Folly

4.9 0.0 smcdel VS Folly

First order logic in Haskell
obdd

4.8 2.8 smcdel VS obdd

pure Haskell implementation of reduced ordered binary decision diagrams
structural-induction

3.5 0.0 smcdel VS structural-induction

SII: Structural Induction Instantiator over any strictly-positive algebraic data type.
tpdb

3.1 2.1 smcdel VS tpdb

parser and prettyprinter for TPDB syntax (termination problem data base)
g4ip-prover

3.1 0.0 smcdel VS g4ip-prover

Theorem prover for intuitionistic propositional logic, fork of github.com/cacay/G4ip
qed

2.7 0.0 smcdel VS qed

Experiments writing a prover
satchmo

2.1 4.0 smcdel VS satchmo

SAT encoder
minisat

2.1 2.4 smcdel VS minisat

Minisat Haskell bundle
g4ip

1.6 0.0 smcdel VS g4ip

A theorem prover using G4ip
judge

0.8 0.0 smcdel VS judge

Tableau-based theorem prover for justification logic.
haskhol-core

0.7 0.0 smcdel VS haskhol-core

The core logical system of the HaskHOL theorem prover. See haskhol.org for more details.

* 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?

Add another 'Logic' Package

Popular Comparisons

README

SMCDEL

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](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.