About Counterdog - Theorem-prover for Counterfactual Datalog
Counterdog is an automated theorem-prover for a counterfactual meta-logic about propositional Datalog programs. It is useful, for example, for reasoning about Datalog-based trust management and authorization languages.