SPL Format Reference

SPL (Spindle Lisp) is a LISP-based DSL for defeasible logic with support for advanced features like variables, temporal reasoning, and metadata.

File Extension

.spl

Comments

Semicolon to end of line:

; This is a comment
(given bird)  ; Inline comment

Grammar Overview

theory      = statement*
statement   = fact | rule | prefer | meta
fact        = "(given" literal ")"
rule        = "(" keyword label? body head ")"
keyword     = "always" | "normally" | "except"
prefer      = "(prefer" label+ ")"
meta        = "(meta" label property* ")"
literal     = atom | "(" atom arg* ")" | "(not" literal ")"
body        = literal | "(and" literal+ ")"
atom        = identifier | variable
variable    = "?" identifier

Facts

Simple Facts

(given bird)
(given penguin)
(given (not guilty))

Predicate Facts

(given (parent alice bob))
(given (employed alice acme))

Flat Predicate Syntax

(given parent alice bob)     ; Same as (given (parent alice bob))
(given employed alice acme)

Rules

Strict Rules (always)

(always r1 penguin bird)
(always r2 (and human mortal) dies)

Defeasible Rules (normally)

(normally r1 bird flies)
(normally r2 penguin (not flies))

Defeaters (except)

(except d1 broken-wing flies)

Unlabeled Rules

Labels are optional (auto-generated):

(normally bird flies)        ; Gets label like "r1"
(always penguin bird)        ; Gets label like "s1"

Literals

Simple

bird
flies
has-feathers

Negated

(not flies)
(not (parent alice bob))

Or with prefix:

~flies

Predicates with Arguments

(parent alice bob)
(employed ?x acme)
(ancestor ?x ?z)

Conjunction

Use and for multiple conditions:

(normally r1 (and bird healthy) flies)
(normally r2 (and student employed) busy)

Variables

Variables start with ?:

(given (parent alice bob))
(given (parent bob charlie))

; Transitive closure
(normally r1 (parent ?x ?y) (ancestor ?x ?y))
(normally r2 (and (parent ?x ?y) (ancestor ?y ?z)) (ancestor ?x ?z))

Wildcard

Use _ to match anything:

(normally r1 (parent _ ?y) (has-parent ?y))

Superiority

Two Rules

(prefer r2 r1)    ; r2 > r1

Chain

(prefer r3 r2 r1)  ; r3 > r2 > r1

Expands to:

(prefer r3 r2)
(prefer r2 r1)

Metadata

Attach metadata to rules:

(meta r1
  (description "Birds normally fly")
  (confidence 0.9)
  (source "ornithology-handbook"))

Properties

(meta rule-label
  (key "string value")
  (key2 ("list" "of" "values")))

Modal Operators

Obligation (must)

(normally signed-contract (must pay))

Permission (may)

(normally member (may access))

Forbidden (forbidden)

(normally unauthorized (forbidden enter))

Temporal Reasoning

Time Points

(moment 2024)                    ; Year
(moment 2024 6 15)               ; Year, month, day
(moment 2024 6 15 14 30 0 "UTC") ; Full timestamp
(moment "2024-06-15T14:30:00Z")  ; ISO 8601
inf                              ; Positive infinity
-inf                             ; Negative infinity

During

(given (during bird 1 10))
(given (during (employed alice acme) (moment 2020) (moment 2023)))

Allen Relations

All 13 Allen interval relations:

(before ?t1 ?t2)       ; t1 ends before t2 starts
(after ?t1 ?t2)        ; t1 starts after t2 ends
(meets ?t1 ?t2)        ; t1 ends exactly when t2 starts
(met-by ?t1 ?t2)       ; t1 starts exactly when t2 ends
(overlaps ?t1 ?t2)     ; t1 starts before t2, ends during t2
(overlapped-by ?t1 ?t2)
(contains ?t1 ?t2)     ; t1 strictly contains t2
(within ?t1 ?t2)       ; t1 is strictly within t2
(starts ?t1 ?t2)       ; Same start, t1 ends first
(started-by ?t1 ?t2)
(finishes ?t1 ?t2)     ; t1 starts after t2, same end
(finished-by ?t1 ?t2)
(equals ?t1 ?t2)       ; Same start and end

Complete Example

; The Penguin Example

; Facts
(given bird)
(given penguin)

; Strict rule
(always s1 penguin bird)

; Defeasible rules
(normally r1 bird flies)
(normally r2 bird has-feathers)
(normally r3 penguin (not flies))
(normally r4 penguin swims)

; Superiority
(prefer r3 r1)

; Defeater
(except d1 broken-wing flies)

; Metadata
(meta r1 (description "Birds typically fly"))
(meta r3 (description "Penguins are an exception"))

DFL vs SPL Comparison