SPINguile - SPINdle for GNU Guile

A GNU Guile implementation of SPINdle, a defeasible logic reasoning system.

Overview

SPINguile is a port of SPINdle Racket v1.6.0 to GNU Guile Scheme. It implements reasoners to compute the consequences of theories in defeasible logic, including:

• Core Reasoning - Basic and modal defeasible logic
• Dual Syntax - Both DFL (Defeasible Logic Format) and SPL (Spindle Lisp) parsers
• Temporal Reasoning - Allen's 13 interval relations with ISO 8601 timestamps
• Trust-Weighted Reasoning - Source identity tracking and trust policies
• Query Operations - Explain, why-not, abduction, what-if, and validation
• Process Mining - Alpha algorithm for discovering rules from event logs
• First-Order Grounding - Datalog-style variable substitution

Original SPINdle Copyright (C) 2009-2014 NICTA Ltd.

Requirements

• GNU Guile 3.0 or later
• SRFI-1 (List library)
• SRFI-9 (Record types)
• SRFI-64 (Testing framework)
• SRFI-69 (Hash tables)

All SRFIs are included with GNU Guile by default.

Optional Dependencies

• guile-json - Required for process mining JSON event log parsing

# macOS with Homebrew
brew install guile-json

# Guix
guix install guile-json

# From source
# https://github.com/aconchillo/guile-json

Installation

git clone https://gitlab.com/thelabph/spinguile.git
cd spinguile

Quick Start

Using DFL Syntax

(add-to-load-path "/path/to/spinguile")
(use-modules (src spindle))

;; Classic penguin example
(define theory (parse-dfl "
  f1: >> penguin
  r1: penguin => bird
  r2: bird => flies
  r3: penguin => -flies
  r3 > r2
"))

(define conclusions (reason theory))
(for-each (lambda (c) (display (conclusion->string c)) (newline))
          conclusions)
;; Output: +D penguin, +d bird, +d -flies

Using SPL Syntax

(use-modules (src lang main))

;; Same theory in SPL
(define conclusions (reason-spl-string "
  (given penguin)
  (normally r1 penguin bird)
  (normally r2 bird flies)
  (normally r3 penguin (not flies))
  (prefer r3 r2)
"))

Running Tests

# Run all tests (208 tests)
guile -L . tests/run-tests.scm

# Run specific test suite
guile -L . tests/spindle-tests.scm      # Core reasoning (37 tests)
guile -L . tests/spl-parser-tests.scm   # SPL parser (29 tests)
guile -L . tests/temporal-tests.scm     # Temporal (41 tests)
guile -L . tests/trust-tests.scm        # Trust-weighted (33 tests)
guile -L . tests/query-tests.scm        # Query operations (27 tests)
guile -L . tests/equivalence-tests.scm  # Racket compatibility (23 tests)
guile -L . tests/integration-tests.scm  # Integration (18 tests)
guile -L . tests/spl-temporal-allen-tests.scm  # Allen interval relations

DFL Syntax

The Defeasible Logic Format (DFL) syntax:

Construct	Syntax	Example
Fact	>> literal	f1: >> bird
Strict Rule	body -> head	r1: bird -> animal
Defeasible Rule	body => head	r2: bird => flies
Defeater	body ~> head	r3: injured ~> -flies
Superiority	rule1 > rule2	r3 > r2
Negation	-literal or ~literal	-flies
Comments	# text	# penguin example

Example DFL Theory

# Classic penguin example
f1: >> tweety
f2: >> penguin
r1: tweety => bird
r2: bird => flies
r3: penguin => -flies
r3 > r2

SPL Syntax

Spindle Lisp (SPL) uses S-expressions:

Construct	Syntax
Fact	(given literal)
Strict Rule	(always label body head)
Defeasible Rule	(normally label body head)
Defeater	(except label body head)
Superiority	(prefer superior inferior)
Negation	(not literal)
Predicate	(predicate arg1 arg2 ...)

Example SPL Theory

(given tweety)
(given penguin)
(normally r1 tweety bird)
(normally r2 bird flies)
(normally r3 penguin (not flies))
(prefer r3 r2)

Module Structure

spinguile/
├── main.scm                 # Entry point
├── Makefile                 # Build targets
├── src/
│   ├── spindle.scm         # Core reasoning engine
│   ├── parser/             # DFL parser
│   │   ├── ast.scm         # AST definitions
│   │   ├── lexer.scm       # Tokenizer
│   │   ├── parser.scm      # Recursive descent parser
│   │   └── main.scm        # Parser interface
│   ├── lang/               # SPL parser
│   │   ├── spl-lexer.scm   # SPL tokenizer
│   │   ├── spl-parser.scm  # SPL parser
│   │   ├── imports.scm     # Import handling
│   │   └── main.scm        # Language interface
│   ├── temporal.scm        # Temporal intervals
│   ├── moment.scm          # ISO 8601 timestamps
│   ├── modal.scm           # Modal logic operators
│   ├── grounding.scm       # First-order grounding
│   ├── trust/              # Trust-weighted reasoning
│   │   ├── source.scm      # Source identity
│   │   ├── structs.scm     # Data structures
│   │   ├── policy.scm      # Trust policies
│   │   └── reason.scm      # Weighted reasoning
│   ├── query/              # Query operations
│   │   ├── structs.scm     # Query data structures
│   │   ├── query.scm       # Basic queries
│   │   ├── explain.scm     # Derivation explanation
│   │   ├── why-not.scm     # Blocking analysis
│   │   ├── abduction.scm   # Abductive reasoning
│   │   ├── what-if.scm     # Hypothetical reasoning
│   │   └── validate.scm    # Theory validation
│   ├── mining/             # Process mining
│   │   ├── event-log.scm   # Event log structures
│   │   ├── footprint.scm   # Footprint matrix
│   │   ├── alpha.scm       # Alpha algorithm
│   │   ├── dfl-convert.scm # Convert to DFL
│   │   └── result.scm      # Mining results
│   ├── cli.scm             # Command-line interface
│   ├── repl.scm            # Interactive REPL
│   └── export.scm          # Export utilities
├── tests/                   # Test suites
├── wasm/                    # WebAssembly support
├── specs/                   # Requirement specifications
│   ├── REQ-003-temporal-defeasible-logic.md
│   ├── REQ-004-modal-operator-support.md
│   └── REQ-005-argumentation-theories.md
└── src/test-theories/       # Example DFL files

API Reference

Core Reasoning

(use-modules (src spindle))

;; Parse and reason
(parse-dfl string)              ; Parse DFL -> theory
(reason theory)                 ; Compute conclusions

;; Literals
(simple-literal name)           ; Create positive literal
(negated-literal name)          ; Create negated literal
(literal-name lit)              ; Get literal name
(literal-negated? lit)          ; Check if negated

;; Rules
(make-fact label literal)       ; Create fact
(simple-rule label type body head) ; Create rule

;; Theory
(empty-theory)                  ; Empty theory
(theory-add-rule theory rule)   ; Add rule
(theory-add-superiority theory sup) ; Add superiority

;; Conclusions
(conclusion-contains? conclusions type literal)
(conclusion->string conclusion)

SPL Language

(use-modules (src lang main))

(reason-spl-string spl)         ; Parse SPL and reason
(reason-spl-file path)          ; Load file and reason
(parse-spl-string spl)          ; Parse SPL -> AST
(spl-ast-to-theory ast)         ; Convert AST -> theory

Temporal Reasoning

(use-modules (src temporal) (src moment))

;; Moments (ISO 8601)
(moment year month day hour min sec tz)
(parse-moment "2026-01-22T10:30:00Z")
(moment-epoch m)                ; Unix timestamp

;; Intervals
(make-interval start end)
(temporal-active-at? interval moment)

;; Allen's Relations
(temporal-before? a b)
(temporal-meets? a b)
(temporal-overlaps? a b)
(temporal-during? a b)
(temporal-starts? a b)
(temporal-finishes? a b)
(temporal-equals? a b)

Trust-Weighted Reasoning

(use-modules (src trust source)
             (src trust policy)
             (src trust reason))

;; Sources
(make-source 'agent "alice")
(parse-source "agent:security")

;; Policies
(make-trust-policy trust-map threshold-map decay-map default)
(extract-trust-policy theory)

;; Reasoning
(reason-with-trust theory policy)
(conclusions-above-threshold conclusions "high")

Query Operations

(use-modules (src query query)
             (src query explain)
             (src query why-not)
             (src query abduction)
             (src query what-if)
             (src query validate))

;; Explain derivation
(explain-conclusion theory conclusions literal)

;; Why not provable
(why-not-provable theory conclusions literal)

;; Abduction - what facts needed?
(requires theory goal)

;; What-if analysis
(what-if-add-fact theory fact)
(what-if-remove-fact theory fact-label)
(what-if-add-rule theory rule)

;; Validation
(validate-theory theory)

Conclusion Types

Symbol	Meaning
+D	Definitely provable
-D	Definitely not provable
+d	Defeasibly provable
-d	Defeasibly not provable

WebAssembly Support

SPINguile compiles to WebAssembly via Guile Hoot.

# Install Hoot
brew tap aconchillo/guile && brew install guile-hoot

# Build WASM
make wasm

# Serve locally
make wasm-serve
# Open http://localhost:8088

Differences from Racket Version

Feature	Racket	Guile
Records	struct	SRFI-9 define-record-type
Parser	parser-tools/yacc	Recursive descent
Lexer	parser-tools/lex	Custom tokenizer
Pattern Matching	racket/match	(ice-9 match)
Hash Tables	hash	SRFI-69
Testing	rackunit	SRFI-64

Related Projects

• spindle-racket - The original Racket implementation this port is based on

License

Original SPINdle implementation is Copyright (C) 2009-2014 NICTA Ltd. This Guile port follows the same licensing terms.