),
examines if M ⊨ φ (i.e., ⊨ M → φ) holds or not, and then
returns either "claim holds" (M ⊨ φ holds) or "claim does not hold"
- --model
-
reads a model from
- --reachability
-
check reachability (i.e., M ∧ φ ≠ empty), instead of entailment.
- -v, --verbose
-
become verbose
- -h, --help
-
show usage
rulessat, ldlmc
LDLTools development team at IBM Research.
(C) Copyright IBM Corp. 2018.
License Apache 2.0.
This is free software: you are free to change and redistribute it.
There is NO WARRANTY, to the extent permitted by law.