Defeasible logic (DL) is an efficient nonmonotonic logic. In the last few years, several variants of DL have been presented to deal with different, and sometimes incompatible, intuitions of nonmonotonic reasoning [1]. This paper discusses the basic variant developed in Billington [2] and Antoniou et al. [3], proposes a computational model based on computer assisted knowledge engineering (CAKE) programs for it, and investigates two semantics (stratified and well founded) for the CAKE programs corresponding to DL theories.

A DL theory consists of facts, rules (strict rules, defeasible rules, and defeaters), and a superiority relation over the rules used to resolve conflicts among rules. DL has a constructive proof theory that is able to classify conclusions of a DL theory into four classes: definitely provable, definitely nonprovable, defeasibly provable, and defeasibly nonprovable. For a definitely/defeasible provable, literal DL shows that every strict/defeasible proof fails.

A CAKE program is comprised of a set of rules and facts about “information granules,” where an information granule partitions the extension of a predicate into three sets: the tuples known to satisfy the predicate, the tuples for which the predicate is known to be false, and the remaining tuples. Relationships between the various granules are then established via a voting mechanism. A predicate is true for a tuple if it is true in at least one module and false in none, false when it is false in at least one granule and true in none, and otherwise its truth value is unknown.

A defeasible theory is transformed in a CAKE program by first introducing predicates corresponding to the degrees of provability in DL; each rule then generates an information granule used to label the provability predicate, and a corresponding rule in CAKE. The inference mechanism of DL is simulated by a set of voting rules; unfortunately the voting rules do not correspond to the variant of DL presented in the paper, where rules can form a team to defeat conflicting rules, but to a different variant without this property, and where only a single stronger rule can defeat rules conflicting with it [1]. The paper discusses stratified semantics for DL, and points out that DL has problems when rules exhibit cyclic dependencies. To obviate this problem, the authors propose well-founded semantics for DL, and present a fixed-point construction to compute the semantics.

The authors seem to be unaware of previous work by Grof [4] and Maher and Governatori [5] on the two semantics. Grof introduces the stratified semantics, and Maher and Governatori present Kunen, and well-founded semantics for DL. On the positive side, the paper presents a different computation method for well-founded semantics, and demonstrates a relationship between two formalisms, the CAKE system and DL, to represent and reason about incomplete information, even if a more accurate analysis of the relationships is needed.