Counterdog: Theorem Prover for Counterfactual Datalog Logic

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.


File NameCounterdog.msi
Date Published24 November 2011
Download Size4.32 MB

Note By installing, copying, or otherwise using this software, you agree to be bound by the terms of its license. Read the license.