SPINdle Racket Implementation

A comprehensive Racket implementation of the SPINdle defeasible logic reasoning system with trust-weighted reasoning and first-order logic support.

Overview

This project provides a complete Racket port of SPINdle (version 2.2.4), a defeasible logic reasoning system originally developed by NICTA. SPINdle implements non-monotonic reasoning capabilities, allowing for conclusions that can be defeated by stronger evidence or superior rules.

Current version: 1.4.0

Features

• Complete Defeasible Logic Implementation

  • Facts (>>), Strict rules (->), Defeasible rules (=>), Defeaters (~>)
  • Superiority relations (>) for conflict resolution
  • Definite (+D/-D) and defeasible (+d/-d) provability levels

• #lang spindle - Racket Language Integration

  • Native Racket language module for writing theories
  • LISP-style syntax: (given bird), (normally r1 bird flies), (prefer r2 r1)
  • Seamless integration with Racket tooling (DrRacket, raco)

• First-Order Variable Support

  • Datalog-style bottom-up grounding
  • Variables prefixed with ? (e.g., ?x, ?person)
  • Automatic instantiation against known facts

• Trust-Weighted Reasoning

  • Source identity tracking (agent, system, external sources)
  • Trust policies with configurable trust values
  • Decay models for time-based trust degradation
  • Threshold-based conclusion filtering
  • Claims blocks for provenance tracking

• Modular Theory Composition

  • @import declarations for importing other DFL files
  • Imported theories are evaluated and conclusions become facts
  • Namespace prefixing to avoid name collisions
  • Nested imports with cycle detection

• Advanced Reasoning Capabilities

  • Forward chaining through rule dependencies
  • Conflict detection and resolution via superiority
  • Cycle detection to prevent infinite loops
  • Modal logic support with operators like [O] (obligation), [P] (permission)
  • Temporal logic support with moment timestamps for time-based reasoning

• Query Operations

  • Interactive query function for checking literal status
  • what-if analysis for hypothetical reasoning
  • why-not explanations for unprovable conclusions
  • Abductive reasoning for finding minimal explanations

• DFL Format Parser

  • Full support for Defeasible Logic Format (DFL) files
  • Comment handling and robust error recovery
  • Modal and temporal literal parsing

• Comprehensive Test Suite

  • 800+ test cases covering all functionality
  • Tests ported from original Java SPINdle implementation
  • Performance and scalability testing
  • Edge case handling (cycles, empty theories, etc.)

Installation

Prerequisites

• Racket 7.0 or later

Installing from Source

git clone <repository-url>
cd spindle-racket
raco pkg install

Usage

Basic Usage

#lang racket
(require "spindle.rkt")
;; Parse a theory from DFL format
(define theory-str 
 "f1: >> bird
 r1: bird => flies
 r2: bird => ¬flies
 r1 > r2")
(define theory (parse-dfl theory-str))
;; Perform reasoning
(define conclusions (reason theory))
;; Check if literal is provable
(define flies (simple-literal "flies"))
(conclusion-contains? conclusions CONCLUSION-DEFEASIBLE-PROVABLE flies)

Using #lang spindle

The recommended way to write theories is using the native Racket language module:

#lang spindle
;; Classic penguin example
(given bird)
(given penguin)
(normally r1 bird flies)
(normally r2 penguin (not flies))
(prefer r2 r1)

The module provides spindle-theory, spindle-conclusions, and spindle-reason:

racket -e '(require "penguin.spl") (spindle-conclusions)'

SPL Syntax Reference

Loading Theory Files (DFL format)

;; Load theory from file
(define theory (parse-dfl-file "examples/penguin.dfl"))
(define conclusions (reason theory))

Importing Other Theories

SPINdle supports modular theory composition through @import declarations. Imported theories are fully evaluated and their conclusions are injected as facts into the importing theory.

;; Load theory with import resolution
(define theory (parse-dfl-file-with-imports "examples/main-theory.dfl"))
(define conclusions (reason theory))

Example DFL files:

# base-knowledge.dfl
>> bird
r1: bird => flies

# main-theory.dfl
@import "./base-knowledge.dfl" .
# Build on imported conclusions
r2: flies => happy

When main-theory.dfl is loaded with parse-dfl-file-with-imports:

1. base-knowledge.dfl is parsed and evaluated
2. Its conclusions (+D bird, +d flies) become facts in main-theory.dfl
3. The rule r2 can then derive +d happy

Prefixed Imports

Use as to namespace imported conclusions and avoid conflicts:

@import "./module-a.dfl" as a .
@import "./module-b.dfl" as b .
# Use prefixed literals
r1: a:flies, b:swims => amphibious

Working with Conclusions

;; Filter conclusions by type
(define definite-conclusions
 (filter-conclusions conclusions CONCLUSION-DEFINITE-PROVABLE))
(define defeasible-conclusions
 (filter-conclusions conclusions CONCLUSION-DEFEASIBLE-PROVABLE))
;; Display all conclusions
(display-conclusions conclusions)

Running the Demo

To see SPINdle in action:

# Run the main demo (parses a theory and shows conclusions)
racket main.rkt
# Run the explanation system demo (recommended)
racket demo.rkt

The explanation demo (demo.rkt) showcases:

• Natural language explanations showing subject and derivation chain
• Conflict resolution with superiority relations
• Medical treatment example with provenance tracking
• JSON-LD and DOT/GraphViz output formats

You can also run individual demos:

racket -e '(require "demo.rkt") (demo-birds-fly)'
racket -e '(require "demo.rkt") (demo-penguin)'
racket -e '(require "demo.rkt") (demo-medical)'

Generating Explanations

SPINdle can generate natural language explanations for its conclusions, showing the reasoning chain and conflict resolution:

(require "spindle.rkt")
(require "src/explanation.rkt")
;; Medical treatment example with annotations
(define theory-str "
@prefix dc: <http://purl.org/dc/terms/> .
---
@id: :fact-condition
dc:description: \"Patient presents with condition X\"---
f1: >> hasConditionX
---
@id: :fact-allergy
dc:description: \"Patient has known allergy to treatment A\"---
f2: >> allergicToA
---
@id: :rule-treatment
dc:description: \"Patients with condition X should receive treatment A\"---
r1: hasConditionX => recommendTreatmentA
---
@id: :rule-contraindication
dc:description: \"Allergy to treatment A contraindicates its use\"---
r2: allergicToA => ¬recommendTreatmentA
---
@id: :rule-alternative
dc:description: \"When treatment A is contraindicated, recommend B\"---
r3: hasConditionX, ¬recommendTreatmentA => recommendTreatmentB
---
@id: :sup-safety
spindle:justification: \"Patient safety takes precedence\"---
r2 > r1
")
(define theory (parse-dfl theory-str))
(define explained-conclusions (reason-with-explanations theory))
;; Find and explain the treatment B recommendation
(define treatmentB-ec
 (findf (lambda (ec)
 (string=? (literal-name (explained-conclusion-literal ec))
 "recommendTreatmentB"))
 explained-conclusions))
(displayln (explanation->natural-language
 (explained-conclusion-explanation treatmentB-ec)))

Output:

═══ CONCLUSION ═══
Literal: "recommendTreatmentB"
Status: Defeasibly Provable (+d)
Meaning: This was proven using defeasible rules and was not defeated.
═══ DERIVATION ═══
1. "recommendTreatmentB" was derived defeasibly
 Using defeasible rule: r3
 Description: When treatment A is contraindicated, recommend B
 Prerequisites:
 1.1. "hasConditionX" was established as a fact
 Using fact: f1
 Description: Patient presents with condition X
 1.2. "NOT recommendTreatmentA" was derived defeasibly
 Using defeasible rule: r2
 Description: Allergy to treatment A contraindicates its use
═══ CONFLICTS RESOLVED ═══
• Rule "r2" defeated rule "r1"
 Resolution method: Explicit superiority declaration
 Superiority relation: :sup-safety
 Justification: Patient safety takes precedence

Other output formats are available:

;; JSON-LD for linked data integration
(explanation->jsonld expl)
;; GraphViz DOT for visualization
(explanation->dot expl)

Running Tests

The implementation includes a comprehensive test suite:

# Run all tests
raco test .
# Run specific test file
racket tests/spindle-tests.rkt
# Run tests programmatically
racket -e "(require \"tests/spindle-tests.rkt\") (run-all-tests)"

Theory Format (DFL)

The Defeasible Logic Format supports the following constructs:

Import Declarations

Import other DFL files to build modular theories:

@import "./path/to/module.dfl" . # Basic import
@import "./module.dfl" as prefix . # Prefixed import
@import <./module.dfl> . # URI-style path

Import declarations must appear at the top of the file, before any rules or facts.

Rule Types

• Facts: f1: >> literal - Definitely true
• Strict Rules: r1: antecedent -> consequent - Must hold if antecedent is true
• Defeasible Rules: r1: antecedent => consequent - Normally holds unless defeated
• Defeaters: r1: antecedent ~> consequent - Blocks conclusions without proving anything

Superiority Relations

r1 > r2 # Rule r1 is superior to rule r2

Multiple Antecedents

r1: p, q, r => s # Rule fires when all of p, q, and r are provable

Modal Literals

f1: >> [O]obligation # Obligation modal
f2: >> [P]permission # Permission modal

Negation

f1: >> ¬literal # Negated literal

Examples

Classic Penguin Example

# Facts
f1: >> tweety
f2: >> penguin
# Rules 
r1: tweety => bird
r2: bird => flies
r3: penguin => ¬flies
# Superiority - penguins override general bird rule
r3 > r2

Conflict Resolution

# Basic conflict with superiority
f1: >> bird
r1: bird => flies
r2: bird => ¬flies
r1 > r2 # r1 wins, so bird flies

Defeater Example

f1: >> context
r1: context => conclusion
r2: context ~> ¬conclusion # Defeater blocks r1 without proving ¬conclusion

First-Order Variables Example

Use ?-prefixed variables for Datalog-style rules that ground against facts:

#lang spindle
;; Facts about family relationships
(given (parent alice bob))
(given (parent bob charlie))
;; Rule with variables - grounds against matching facts
(normally r1 (parent ?x ?y) (ancestor ?x ?y))
(normally r2 (and (parent ?x ?y) (ancestor ?y ?z)) (ancestor ?x ?z))

Variables are automatically instantiated against known facts using bottom-up grounding.

Trust-Weighted Reasoning Example

Track source provenance and assign trust weights to conclusions:

#lang spindle
;; Claims block attributes facts to a source
(claims "agent:alice" "2026年01月15日T10:00:00Z"
 (given raining))
(claims "agent:bob" "2026年01月15日T10:30:00Z"
 (given (not raining)))
;; Trust policy defines trust weights
(given (trusts "agent:alice" 0.9))
(given (trusts "agent:bob" 0.6))
;; Threshold for acceptance
(given (threshold raining 0.7))

Use reason-with-trust to get weighted conclusions:

(require spindle/trust)
(define results (reason-with-trust object-theory trust-policy-theory))
(define above-threshold (conclusions-above-threshold results))

Modular Theory Example

Building a layered reasoning system with imports:

# facts/patient.dfl - Patient data layer
>> hasConditionX
>> allergicToA

# rules/contraindications.dfl - Medical rules layer
@import "../facts/patient.dfl" .
r1: allergicToA => contraindicatedA
r2: hasConditionX => recommendTreatmentA

# main.dfl - Main reasoning
@import "./rules/contraindications.dfl" as med .
# Override recommendation when contraindicated
r1: med:contraindicatedA, med:recommendTreatmentA => recommendTreatmentB

Query Operations

Interactive querying and analysis of theories:

(require spindle/query)
;; Check if a literal holds
(query theory 'flies) ; => #t, #f, or 'unknown
;; What-if analysis - hypothetical reasoning
(what-if theory '((given sunny)) 'goes-outside)
;; Why-not - explain why a literal wasn't proven
(why-not theory 'flies)
;; Abduction - find minimal facts to prove a goal
(abduce theory 'goal)

Architecture

The implementation consists of several key modules:

• Core (src/spindle.rkt): Data structures for literals, rules, theories, and conclusions
• Parser (src/parser/): DFL format parser with robust error handling
• Language (src/lang/): #lang spindle implementation with SPL lexer/parser
• Reasoning Engine: Forward chaining with cycle detection
• Trust Module (src/trust/): Source identity, trust policies, and weighted reasoning
• Query Module (src/query/): Interactive query operations, what-if, why-not, abduction
• Grounding (src/grounding.rkt): First-order variable support via Datalog grounding
• Temporal (src/moment.rkt, src/temporal.rkt): Timestamp parsing and temporal reasoning
• Test Suite: 800+ tests covering all functionality

Performance

The implementation includes cycle detection and optimization for:

• Self-referential rules
• Circular rule dependencies
• Large theory processing
• Memory-efficient conclusion tracking

Compatibility

This implementation maintains compatibility with:

• Original Java SPINdle 2.2.4 theory files
• Standard DFL format specifications
• Modal and temporal reasoning extensions
• Native Racket integration via #lang spindle (SPL format)

License

SPINdle uses GNU Lesser General Public License v3.

Contributing

1. Fork the repository
2. Create a feature branch
3. Add tests for new functionality
4. Ensure all tests pass: raco test .
5. Submit a pull request

References

• Original SPINdle: SPINdle Project
• Defeasible Logic: Nute, D. (1994). "Defeasible Logic"
• DFL Format: [Defeasible Logic Format Specification]

Support

For issues and questions:

• Check the test suite for usage examples
• Review the comprehensive inline documentation
• File issues on the project repository

This Racket implementation provides a faithful port of the SPINdle defeasible logic reasoning system, extended with temporal logic, trust-weighted reasoning, abductive reasoning, first-order variable support, and native Racket language integration.