5.1 Facts🔗ℹ

Use given to declare facts:

(given bird)

(given penguin)

5.2 Rules🔗ℹ

5.3 Negation🔗ℹ

Use not for negated literals:

(not flies)

(normally r1 penguin (not flies))

5.4 Superiority🔗ℹ

Use prefer to declare which rules win conflicts:

(prefer r2 r1)                ; r2 defeats r1

5.5 Multiple Premises🔗ℹ

Wrap multiple premises in a list:

(normally r1 (fever cough) has-flu)

(always r2 (a b c) conclusion)

5.6 Comments🔗ℹ

Use semicolons for comments:

; This is a comment

(given bird)  ; Inline comment

5.7 Modal Operators🔗ℹ

SPL supports deontic modal operators:

(must pay-taxes)              ; Obligation

(may access-resource)         ; Permission

(forbidden enter-restricted)  ; Prohibition

In rules:

(normally r1 employee (must attend-meetings))

(normally r2 member (may access-library))

5.8 Using #lang spindle🔗ℹ

Create .spl files with the #lang spindle directive:

"theory.spl"

#lang spindle

(given bird)

(given penguin)

(normally r1 bird flies)

(normally r2 penguin (not flies))

(prefer r2 r1)

Then use in Racket:

(require "theory.spl")

(spindle-conclusions)

5.9 Programmatic Use🔗ℹ

(require spindle/lang)

(define conclusions

(reason-spl-string

"(given bird)\n    (normally r1 bird flies)"))

(reason-spl-file "theory.spl")

5.10 Complete Example🔗ℹ

#lang spindle

; Medical diagnosis example

; Patient symptoms

(given has-fever)

(given has-cough)

(given has-rash)

; Diagnostic rules

(normally r1 (has-fever has-cough) has-flu)

(normally r2 (has-fever has-rash) has-measles)

(normally r3 has-measles (not has-flu))

; Measles is more specific diagnosis

(prefer r3 r1)

5.11 SPL vs DFL Comparison🔗ℹ