▼Spindle:   Defeasible Logic Reasoning
►6 Query Operations
On this page:
6.1 Basic Queries
query
query-literal
6.2 Theory Status
status
6.3 Explanations
explain
6.4 Why-Not Queries
why-not
6.5 Abductive Queries
requires
6.6 Hypothetical Reasoning
what-if
6.7 Theory Validation
validate
6.8 REPL Integration
load-theory
repl-query
repl-explain
repl-why-not
repl-status
9.0
  top  contents    up   

6 Query Operations🔗ℹ

 (require spindle/query) package: spindle

Spindle provides interactive query operations for exploring theories and understanding reasoning results.

6.1 Basic Queries🔗ℹ

procedure

(query th lit) → (or/c #t #f 'unknown)

  th : theory?
  lit : literal?
Query whether a literal holds in the theory. Returns #t if provable, #f if refuted, 'unknown otherwise.

(query my-theory (simple-literal "flies"))

procedure

(query-literal th lit) → query-result?

  th : theory?
  lit : literal?
Full query returning detailed result structure.

6.2 Theory Status🔗ℹ

procedure

(status th) → status-result?

  th : theory?
Get complete status of all conclusions in the theory.

The result categorizes conclusions as:

  • Definitely provable (+D)

  • Definitely not provable (-D)

  • Defeasibly provable (+d)

  • Defeasibly not provable (-d)

6.3 Explanations🔗ℹ

procedure

(explain th lit) → (or/c explanation? #f)

  th : theory?
  lit : literal?
Explain why a literal was concluded.

Returns an explanation with:

  • The derivation tree (proof steps)

  • Sources used in the derivation

  • Trust chain if applicable

6.4 Why-Not Queries🔗ℹ

procedure

(why-not th lit) → why-not-result?

  th : theory?
  lit : literal?
Explain why a literal was not concluded.

Returns information about:

  • Blocking conditions (what prevented derivation)

  • Missing premises

  • Defeating rules

6.5 Abductive Queries🔗ℹ

procedure

(requires th lit) → abduction-result?

  th : theory?
  lit : literal?
Find what facts would be needed to derive a literal.

Returns abduction solutions with:

  • Sets of facts that would make the literal provable

  • Confidence estimates

  • Rules that would be used

6.6 Hypothetical Reasoning🔗ℹ

procedure

(what-if th assumptions query-lit) → what-if-result?

  th : theory?
  assumptions : (listof any/c)
  query-lit : literal?
Test what would happen if certain facts were assumed.

The original theory is not modified.

(what-if my-theory
         '((given tests-pass))
         (simple-literal "ready-deploy"))

6.7 Theory Validation🔗ℹ

procedure

(validate th) → validation-result?

  th : theory?
Check a theory for errors and warnings.

Checks include:

  • Undefined literals in rule bodies

  • Invalid superiority references

  • Duplicate rule IDs

  • Strict rule cycles

  • Contradictory facts

6.8 REPL Integration🔗ℹ

 (require spindle/query/repl) package: spindle

For interactive use, the REPL module provides convenient wrappers:

procedure

(load-theory path) → theory-ref?

  path : path-string?
Load a theory file and set it as current.

procedure

(repl-query lit-sexp) → any/c

  lit-sexp : any/c
Query the current theory using S-expression literal syntax.

(load-theory "my-theory.dfl")
(repl-query 'flies)
(repl-query '(not authorized))

procedure

(repl-explain lit-sexp) → any/c

  lit-sexp : any/c
Explain a conclusion in the current theory.

procedure

(repl-why-not lit-sexp) → any/c

  lit-sexp : any/c
Explain why something is not concluded.

procedure

(repl-status) → status-result?

Get status of current theory.

  top  contents    up