2.1.1 From Package Server🔗ℹ

The easiest way to install Spindle is via the Racket package manager:

  raco pkg install spindle

2.1.2 From Source🔗ℹ

To install from source:

2.1.3 Verify Installation🔗ℹ

Test that Spindle is installed correctly:

  racket -e '(require spindle) (displayln "Spindle installed!")'

2.2.1 Creating a Theory File🔗ℹ

Create a file called birds.dfl with the following content:

"birds.dfl"

# Facts: what we know to be true

>> tweety_is_bird

>> tweety_is_penguin

# Rules: how we reason

r1: tweety_is_bird => tweety_flies

r2: tweety_is_penguin => ¬tweety_flies

# Superiority: which rules win conflicts

r2 > r1

2.2.2 Understanding the Syntax🔗ℹ

• >> literal — Declares a fact (something definitely true)

• label: body => head — A defeasible rule (typically holds)

• label: body -> head — A strict rule (always holds)

• ¬literal — Negation (you can also use -literal)

• r2 > r1 — Rule r2 is superior to r1

2.2.3 Running the Reasoner🔗ℹ

Run the reasoner from Racket:

(require spindle)

(define-values (theory errors)

(parse-dfl-file "birds.dfl"))

(define conclusions (reason theory))

(for ([c conclusions])

(printf "~a: ~a~n"

(conclusion-type c)

(literal->string (conclusion-literal c))))

The reasoner correctly concludes that Tweety does not fly, because the penguin rule defeats the bird rule.

2.3.1 Basic Usage🔗ℹ

(require spindle)

(define-values (theory errors)

(parse-dfl-string ">> bird\nr1: bird => flies"))

(define conclusions (reason theory))

(for ([c conclusions])

(printf "~a: ~a~n"

(conclusion-type c)

(literal->string (conclusion-literal c))))

2.3.2 Using the Unified Interface🔗ℹ

The unified interface auto-detects file format:

(require spindle/unified)

(define conclusions (reason-file "theory.dfl"))

(define conclusions (reason-string "(given bird)" 'spl))

2.3.3 Using SPL Syntax🔗ℹ

If you prefer S-expressions:

(require spindle/lang)

(define conclusions

(reason-spl-string

"(given bird)\n    (given penguin)\n    (normally r1 bird flies)\n    (normally r2 penguin (not flies))\n    (prefer r2 r1)"))