9 Examples
This section provides worked examples of defeasible logic theories.
9.1 The Penguin Example
The classic example of defeasible reasoning: penguins are birds that don’t fly.
9.1.1 DFL Version
"penguin.dfl"
>> bird
>> penguin
r1: bird => flies
r2: penguin => ¬flies
r2 > r1
9.1.2 SPL Version
"penguin.spl"
(given bird) (given penguin) (normally r1 bird flies) (normally r2 penguin (not flies)) (prefer r2 r1)
9.1.3 Running the Example
(require spindle) (define-values (theory errors) (parse-dfl-file "penguin.dfl")) (define conclusions (reason theory)) (for ([c conclusions]) (printf "~a: ~a~n" (conclusion-type c) (literal->string (conclusion-literal c))))
+D: bird |
+D: penguin |
+d: ¬flies |
9.1.4 Explanation
(require spindle spindle/explanation) (define-values (theory errors) (parse-dfl-file "penguin.dfl")) (define conclusions (reason theory)) (define expl (explain theory conclusions (simple-literal "flies" #t))) (displayln (explanation->text expl))
Rule r2 concludes ¬flies from penguin
Rule r1 would conclude flies from bird
But r2 > r1, so r2 defeats r1
9.2 Medical Diagnosis
A simple medical reasoning example with multiple conditions.
"medical.dfl"
>> has_fever
>> has_cough
>> has_rash
r1: has_fever, has_cough => has_flu
r2: has_fever, has_rash => has_measles
r3: has_measles => ¬has_flu
r3 > r1
9.2.1 Analysis
When the patient has fever, cough, AND rash:
(require spindle) (define-values (theory errors) (parse-dfl-file "medical.dfl")) (define conclusions (reason theory))
+D: has_fever |
+D: has_cough |
+D: has_rash |
+d: has_measles |
+d: ¬has_flu |
The measles diagnosis defeats the flu diagnosis because r3 > r1.
9.3 Access Control Policy
A policy-based access control example with exceptions.
"access.dfl"
>> user_alice
>> is_employee
>> is_contractor
>> during_business_hours
r1: is_employee => can_access_intranet
r2: is_contractor => can_access_intranet
r3: is_contractor => ¬can_access_sensitive
r4: during_business_hours, is_employee => can_access_sensitive
r5: is_contractor => ¬can_access_sensitive
r5 > r4
9.4 Using Defeaters
Defeaters block conclusions without asserting the opposite.
"defeater.dfl"
>> bird
>> has_broken_wing
r1: bird => flies
d1: has_broken_wing ~> ¬flies
9.4.1 Defeater vs Defeasible Rule
flies is blocked (not concluded)
¬flies is also NOT concluded
The flying status is simply unknown
¬flies would be actively concluded
You’d need a superiority to resolve the conflict
9.5 Rule Chains
Rules can chain together to derive conclusions.
"chain.dfl"
>> tweety
r1: tweety -> is_bird
r2: is_bird => has_wings
r3: has_wings => can_fly
r4: tweety => is_penguin
r5: is_penguin => ¬can_fly
r5 > r3
The chain tweety → is_bird → has_wings → can_fly is blocked by the penguin exception.