Defeasible Logic

1. G. Antoniou, D. Billington, G. Governatori and M. Maher. Representation Results for Defeasible Logic. ACM Transactions on Computational Logic, 2, 255-287, 2001.

2. M. Maher. Propositional Defeasible Logic has Linear Complexity. Theory and Practice of Logic Programming, 1 (6) 691-711, 2001.

3. D. Nute. Defeasible Logic. In D. M Gabbay, C. J. Hogger and J. A. Robinson (eds.): Handbook of Logic in Artificial Intelligence and Logic Programming, vol. 3, Oxford University Press, 1994, 353-395.

Description of Defeasible Logic

DL – a non-monotonic formalism based on rules and a priority relation on them.

A theory in this logic consists of five components: facts, strict rules, defeasible rules, defeaters and a superiority relation.

Facts – classical logic statements describing indisputable facts, for example “Marco is Italian”

Italian(Marco)  (1)

or “Marco is a communist”

Communist(Marco).  (2)

Strict rules – rules in a classical sense, i.e. if premises of a rule hold then so do the conclusion. An example:

Italian(x) → European(x).  (3)

Defeasible rules are understood in the following way: if premises of a rule hold and the contrary of the conclusion of the rule is unknown, then the conclusion holds.

An example: “Typically, Italians are catholics” represented as

Italian(x) ⇒ Catholic(x).  (4)

The rule (4) together with (1) allows us to conclude that Marco is a catholic.

Consider now the rule

Communist(x) ⇒ ¬Catholic(x).  (5)

Given (5) and (2) we can conclude that Marco is not a catholic. However, if the theory under consideration consists of (1), (2), (4) and (5), we cannot determine whether Marco is a catholic or not.

Defeaters – rules that are not used to draw any conclusions, but to prevent conclusions of some defeasible rules. An example:

Communist(x) ⇝ ¬Catholic(x).  (6)

The intuitive meaning: “for any object x, if x is a communist, then the conclusion that x is a catholic should be blocked.”

From (2) and (6) we cannot conclude that Marco is not a catholic.

However, in the context with (1) and (4), the rule (6) prevent the conclusion that Marco is a catholic.

The superiority relation among rules is used to make one rule stronger than another.

Assumptions:

1. the relation is cycles free

2. is defined locally, i.e. between rules with complementary heads.

For example, consider rules (1), (2), (4) and (5) and the superiority relation (5) > (4). Now, we may conclude that Marco is not a catholic, because the conclusion of (4) is overriden by the conclusion of (5).

Formal definition

Language

A fixed subset of first-order language containing a finite set of constants and a finite set of relations.

Both facts and rules may contain free variables. Such facts (rules) are interpreted as schemata of facts (rules), i.e. as the set of all instances over the set of constants of the considered language.

A defeasible theory D – a triple ⟨F, R, >⟩, where • F is a finite set of literals (called facts),

• R is a finite set of rules,

• > is an acyclic superiority relation on R.

Rules are of the form:

r : A(r) ↪ C(r),

where • r is a unique label of the rule,

• A(r) – its antecedent (body) – a finite list of literals,

• C(r) – its consequent (head) – a single literal, • ↪ depends on a kind of a rule:

↪= \{ \begin{matrix}→ & if it is a strict rule \\ ⇒ & if it is a defeasible rule \\ ⇝ & if it is a defeater \end{matrix}

A superiority relation > is a binary relation on R. r_{1} > r_{2} states that r_{1} overrules r_{2} if both rules are applicable. The relation > is assumed to be acyclic and is defined between rules with complementary heads.

Proof theory

DL is defined by a proof theory. R_{s}, R_{d}, R_{dft} – the subsets of strict rules, defeasible rules and defeaters of R, respectively. R[q] – a set of all rules from R with q in their heads.

A conclusion of a theory D is a tagged literal in one of the forms:

+ Δq – means that q is definitely provable in D.

−Δq – means that we have proved that q is not definitely provable in D.

+δq – means that q is defeasibly provable in D.

−δq – means that we have proved that q is not defeasibly provable in D.

Provability in DL

The notion of provability is based on the concept of a derivation in D = ⟨F, R, >⟩ – a finite sequence P = (P (1), …, P (n)) of tagged literals constructed by inference rules of four kinds. P (1..i) – the initial part of the sequence P of length i.

+Δ : We may append P (i + 1) = +Δq if either (1) q ∈ F or

(2) ∃r ∈ R_{s}[q] ∀a ∈ A(r) : +Δa ∈ P (1..i).

−Δ : We may append P (i + 1) = −Δq if (1) q ∉ F and

(2) ∀r ∈ R_{s}[q] ∃a ∈ A(r) : −Δa ∈ P (1..i).

+δ : We may append P (i + 1) = +δq if either (1) +Δq ∈ P (1..i) or

(2) (2.1) ∃r ∈ R_{sd}[q] ∀a ∈ A(r) : +δa ∈ P (1..i) and (2.2) −Δ¬q ∈ P (1..i) and (2.3) ∀s ∈ R[¬q] either

(2.3.1) ∃a ∈ A(s) : −δa ∈ P (1..i) or (2.3.2) ∃t ∈ R_{sd}[q] such that ∀a ∈ A(t) : +δa ∈ P (1..i) and t > s.

−δ : We may append P (i + 1) = −δq (1) −Δq ∈ P (1..i) and

(2) (2.1) ∀r ∈ R_{sd}[q]∃a ∈ A(r) : −δa ∈ P (1..i) or (2.2) +Δ¬q ∈ P (1..i) or (2.3) ∃s ∈ R[¬q] such that

(2.3.1) ∀a ∈ A(s) : +δa ∈ P (1..i) and (2.3.2) ∀t ∈ R_{sd}[q] either ∃a ∈ A(t) : −δa ∈ P (1..i) or t ≯ s.

An analisis of the proof theory

We may define four sets of literals wrt the types of conclusions of a theory D.

+Δ = {p | D ⊢ +Δp}
−Δ = {p | D ⊢ −Δp}
+δ = {p | D ⊢ +δp}
−δ = {p | D ⊢ −δp}

As straightforward consequences of the proof rules, we have the following relations among the sets.

+Δ ⊆ +δ  +Δ ∩ −Δ = ∅
−δ ⊆ −Δ  +δ ∩ −δ = ∅

Thus, there are six different possible outcomes. A: ⊬ −Δp and ⊬ +δp

p ↦ p B: ⊢ +δp and ⊬ +Δp and ⊬ −Δp

⇒ p; p ↦ p C: ⊢ +Δp (and ⊢ +δp)

↦ p D: ⊢ +δp and ⊢ −Δp

⇒ p E: ⊢ −Δp and ⊬= δp and ⊬ −δp

p ⇒ p F: ⊢ −δp (and ⊢ −Δp)

∅ These outcomes may be represented by the following diagram.

Proposition 1 Consider a defeasible theory D.

1. If ⊬ −Δ¬p and ⊬ +Δp then ⊬ +δp

2. If ⊢ +Δ¬p and ⊢ −Δp then ⊢ −δp

3. If ⊢ +δ¬p and ⊢ −Δp and ⊬ −δp then D is cyclic.

Theorem 1 The consequences of a defeasible theory D can be computed in O(N) time, where N is the number of symbols in D.

Examples

Example 1 Consider a theory ⟨F, R, >⟩, where F = {Italian(Marco), Communist(Marco)} R = {r_{1} : Italian(x) ⇒ Catholic(x), r_{2} : Communist(x) ⇒

¬Catholic(x)} > = {r_{2} > r_{1}} Below is a derivation of +δ¬Catholic(Marco). P = (+ΔItalian(Marco), +δItalian(Marco), +ΔCommunist(Marco),

+δCommunist(Marco), −ΔCatholic(Marco), +δ¬Catholic(Marco)).

Example 2 Consider the following scenario.

John is 17-year-old.

Typically, 17-year-olds are unmarried.

Typically, adults are married. Typically, adults are employed. Typically, employees are adult.

Given the above facts, we intuitively feel that “John is unmarried” should be provable. However, this conclusion cannot be derived in DL.

A DL theory corresponding to the scenario. (Here j, Y 17, A, E and M stand for John, 17 − year − old, Adult, Employed and Married, respectively.)

Y 17(j) A(x) ⇒ E(x) E(x) ⇒ A(x) A(x) ⇒ M(x) Y 17(x) ⇒ ¬M(x).

The conclusion +δ¬M(j) cannot be derived.