Counterdog is an automated theorem prover for counterfactual meta-logic on propositional Datalog. The prover is complete for the logic and can prove or disprove counterfactual statements such as “if ‘p’ is false in a Datalog program but would be true if it contained ‘a:-b,’ then ‘b’ is true in the program.” Counterdog is useful for reasoning about Datalog-based trust-management languages.