▼Spindle:   Defeasible Logic Reasoning
►3 Core API Reference
On this page:
3.1 Literals
literal?
simple-literal
negated-literal
literal-name
literal-negated?
literal->string
negate-literal
3.2 Rules
rule?
RULE-TYPE-FACT
RULE-TYPE-STRICT
RULE-TYPE-DEFEASIBLE
RULE-TYPE-DEFEATER
make-fact
simple-rule
rule-label
rule-type
rule-body
rule-head
rule->string
3.3 Theories
theory?
empty-theory
theory-add-rule
theory-add-superiority
theory-all-rules
theory-superiorities
3.4 Reasoning
reason
reason-with-explanations
3.5 Conclusions
conclusion?
CONCLUSION-DEFINITE-PROVABLE
CONCLUSION-DEFINITE-NOT-PROVABLE
CONCLUSION-DEFEASIBLE-PROVABLE
CONCLUSION-DEFEASIBLE-NOT-PROVABLE
conclusion-type
conclusion-literal
conclusion->string
3.6 Parsing
parse-dfl-string
parse-dfl-file
ast->theory
9.0
  top  contents    up   

3 Core API Reference🔗ℹ

 (require spindle) package: spindle

This section documents the core Spindle API for defeasible logic reasoning.

3.1 Literals🔗ℹ

Literals represent atomic propositions that can be true or false.

procedure

(literal? v) → boolean?

  v : any/c
Returns #t if v is a literal.

procedure

(simple-literal name) → literal?

  name : string?
Creates a simple (non-negated) literal with the given name.

(simple-literal "bird")

procedure

(negated-literal name) → literal?

  name : string?
Creates a negated literal.

(negated-literal "flies")

procedure

(literal-name lit) → string?

  lit : literal?
Returns the name of a literal.

procedure

(literal-negated? lit) → boolean?

  lit : literal?
Returns #t if the literal is negated.

procedure

(literal->string lit) → string?

  lit : literal?
Converts a literal to its string representation.

procedure

(negate-literal lit) → literal?

  lit : literal?
Returns the negation of a literal.

3.2 Rules🔗ℹ

Rules define how conclusions are derived from premises.

procedure

(rule? v) → boolean?

  v : any/c
Returns #t if v is a rule.

value

RULE-TYPE-FACT : symbol?

Rule type for facts (unconditional truths).

value

RULE-TYPE-STRICT : symbol?

Rule type for strict rules (always apply, use ->).

value

RULE-TYPE-DEFEASIBLE : symbol?

Rule type for defeasible rules (can be defeated, use =>).

value

RULE-TYPE-DEFEATER : symbol?

Rule type for defeaters (block but don’t conclude, use ~>).

procedure

(make-fact label literal) → rule?

  label : string?
  literal : literal?
Creates a fact rule.

(make-fact "f1" (simple-literal "bird"))

procedure

(simple-rule label type body head) → rule?

  label : string?
  type : symbol?
  body : (listof literal?)
  head : (listof literal?)
Creates a rule with the given components.

(simple-rule "r1" RULE-TYPE-DEFEASIBLE
             (list (simple-literal "bird"))
             (list (simple-literal "flies")))

procedure

(rule-label r) → string?

  r : rule?
Returns the label of a rule.

procedure

(rule-type r) → symbol?

  r : rule?
Returns the type of a rule.

procedure

(rule-body r) → (listof literal?)

  r : rule?
Returns the body (premises) of a rule.

procedure

(rule-head r) → (listof literal?)

  r : rule?
Returns the head (conclusions) of a rule.

procedure

(rule->string r) → string?

  r : rule?
Converts a rule to its string representation.

3.3 Theories🔗ℹ

A theory is a collection of rules and superiority relations.

procedure

(theory? v) → boolean?

  v : any/c
Returns #t if v is a theory.

procedure

(empty-theory) → theory?

Creates an empty theory.

procedure

(theory-add-rule th r) → theory?

  th : theory?
  r : rule?
Returns a new theory with the rule added.

procedure

(theory-add-superiority th    
  superior    
  inferior) → theory?
  th : theory?
  superior : string?
  inferior : string?
Returns a new theory with a superiority relation added. The superior rule defeats the inferior rule.

procedure

(theory-all-rules th) → (listof rule?)

  th : theory?
Returns all rules in the theory.

procedure

(theory-superiorities th) → (listof superiority?)

  th : theory?
Returns all superiority relations in the theory.

3.4 Reasoning🔗ℹ

The reasoning engine derives conclusions from a theory.

procedure

(reason th) → (listof conclusion?)

  th : theory?
Runs the defeasible reasoning algorithm on the theory. Returns a list of conclusions.

(define conclusions (reason my-theory))
(for ([c conclusions])
  (displayln (conclusion->string c)))

procedure

(reason-with-explanations th) → (listof conclusion?)

  th : theory?
Like reason, but includes explanation data for each conclusion.

3.5 Conclusions🔗ℹ

Conclusions represent the results of reasoning.

procedure

(conclusion? v) → boolean?

  v : any/c
Returns #t if v is a conclusion.

value

CONCLUSION-DEFINITE-PROVABLE : symbol?

Conclusion type: definitely provable (+D).

value

CONCLUSION-DEFINITE-NOT-PROVABLE : symbol?

Conclusion type: definitely not provable (-D).

value

CONCLUSION-DEFEASIBLE-PROVABLE : symbol?

Conclusion type: defeasibly provable (+d).

value

CONCLUSION-DEFEASIBLE-NOT-PROVABLE : symbol?

Conclusion type: defeasibly not provable (-d).

procedure

(conclusion-type c) → symbol?

  c : conclusion?
Returns the type of conclusion.

procedure

(conclusion-literal c) → literal?

  c : conclusion?
Returns the literal that was concluded.

procedure

(conclusion->string c) → string?

  c : conclusion?
Converts a conclusion to its string representation.

3.6 Parsing🔗ℹ

procedure

(parse-dfl-string s) → 
any/c (listof any/c)
  s : string?
Parses a DFL string. Returns two values: the AST and a list of errors.

(define-values (ast errors)
  (parse-dfl-string ">> bird\nr1: bird => flies"))
(when (null? errors)
  (displayln "Parse successful!"))

procedure

(parse-dfl-file path) → 
any/c (listof any/c)
  path : path-string?
Parses a DFL file. Returns two values: the AST and a list of errors.

procedure

(ast->theory ast) → theory?

  ast : any/c
Converts a parsed AST to a runtime theory.

  top  contents    up