Redundancy in logic III: Non-monotonic reasoning Original Research Article

Results about the redundancy of certain versions of circumscription and default logic are presented. In particular, propositional circumscription where all variables are minimized and skeptical default logics are considered. This restricted version of circumscription is shown to have the unitary redundancy property: a CNF formula is redundant (it is equivalent to one of its proper subsets) if and only if it contains a redundant clause (it is equivalent to itself minus one clause); default logic does not have this property in general. We also give the complexity of checking redundancy in the considered formalisms.