 Such rules read as expected, but with a small twist. As usual, the rule licenses its conclusion if the formulas in the antecedent (right hand side) hold. The twist is that the falsity of (default) negated formulas such as penguin need not be positively established: their falsity is assumed in the absence of a proof of the opposite. In our example, if penguin cannot be proved then not penguin is considered to hold (“by default”). A logic program for our Tweety example may consist of the rule above and 