Counterdog is an automated theorem prover for a 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. The theory and implementation were developed by Moritz Y. Becker and Nik Sultana.