Concepts
Defeasible logic is a non-monotonic reasoning system. This chapter introduces the core concepts you need to understand Spindle.
Classical vs. Defeasible Logic
Classical (Monotonic) Logic:
- Once proven, always proven
- Adding facts only adds conclusions
- Cannot handle exceptions
Defeasible (Non-Monotonic) Logic:
- Conclusions are tentative
- New evidence can defeat existing conclusions
- Handles exceptions naturally
The Tweety Problem
The motivating example for defeasible logic:
Tweety is a bird. Tweety is a penguin. Birds fly. Penguins don't fly. Does Tweety fly?
Classical logic produces a contradiction. The declared priority makes "penguins don't fly" override "birds fly." Spindle does not infer this priority automatically from specificity.
(given bird)
(given penguin)
(normally r1 bird flies)
(normally r2 penguin (not flies))
(prefer r2 r1)
Result: Tweety doesn't fly.
Key Terminology
| Term | Definition |
|---|---|
| Literal | An atomic proposition, possibly negated (e.g., flies, -flies) |
| Rule | A conditional statement with body and head |
| Theory | A collection of rules and superiority relations |
| Conclusion | A proven literal with a provability level |
| Defeat | When one rule blocks another's conclusion |
| Superiority | A preference relation between rules |
| Bind | Assigns a computed arithmetic result to a variable |
| Guard | A comparison constraint that filters rule applicability |
Chapters
- Rules and Facts - The four rule types
- Conclusions - Understanding +D, -D, +d, -d
- Superiority - Resolving conflicts
- Negation - Strong negation in Spindle