,
converts them to a LDL formula φ,
examines if φ is satisfiable or not, and then
returns either "valid" (¬φ is unsatisfiable), "satisfiable", or "unsatisfiable"
- -v, --verbose
-
become verbose
- -h, --help
-
show usage
rulesmc, ldlsat
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.