FuXi: Reborn Semantic Web Reasoner & Interlocutor

FuXi CLI subcommand for forward chaining evaluation and RETE network diagnostics.

fuxi.core facts.n3

FuXi CLI subcommand for OWL reasoning, DLP compilation, and BFP query answering. Supports --dlp, --hybrid, --method=bfp, --why (SPARQL goal), --output (proof-graph-svg, man-owl, pml, etc.).

fuxi.owl --method=bfp --dlp --hybrid --ns eg=http://example.net/vocab# --why "ASK { eg:bob your:isBrotherOf eg:joe }" --output proof-graph-svg test/OWL/inverseOf/premises001.rdf > proof.svg

FuXi CLI subcommand for proof and SIP graph generation. Output formats include rete-network-svg, sip-collection-svg, adornment, pml (Provenance Markup Language), proof-graph-svg, proof-graph-png.

fuxi.proof --method=bfp --dlp --hybrid --ns eg=http://example.net/vocab# --why "ASK { eg:bob your:isBrotherOf eg:joe }" --output rete-network-svg test/OWL/inverseOf/premises001.rdf > rete_network.svg

The article's OWL test case 7.1.24 states: "if the pair (x,y) is an instance of P, then the pair (y,x) is an instance of the named property." FuXi's Backward Fixpoint Procedure evaluates the goal ASK { eg:bob your:isBrotherOf eg:joe }. DLP compiles owl:inverseOf into bidirectional Horn rules; BFP rewrites the goal to the sub-goal ASK { eg:joe your:isBrotherOf eg:bob }, dispatches it to the EDB — which confirms the ABox fact — and the goal is proved. This CONSTRUCT materialises that BFP-derived entailment from the named-graph data.

Sample Dataset (FuXi test suite ↗):

inverseOf ABox (premises001.rdf):

@prefix your: <http://example.net/vocab#> .
@prefix eg:   <http://example.net/> .

eg:joe your:isBrotherOf eg:bob .           # ABox asserted fact

inverseOf TBox (owl:inverseOf axiom) (TBox — ontology axioms):

@prefix your: <http://example.net/vocab#> .
@prefix owl:  <http://www.w3.org/2002/07/owl#> .

your:isBrotherOf owl:inverseOf your:isBrotherOf .

# DLP compiles this to bidirectional N3 Horn rules:
# { ?X your:isBrotherOf ?Y } => { ?Y your:isBrotherOf ?X } .

⇒ eg:bob your:isBrotherOf eg:joe ← BFP proves via owl:inverseOf backward chaining

SPARQL expressing this entailment (click ▶ to run live):

PREFIX your: <http://example.net/vocab#>
PREFIX eg:   <http://example.net/>
PREFIX owl:  <http://www.w3.org/2002/07/owl#>

# BFP goal: ASK { eg:bob your:isBrotherOf eg:joe }
# DLP Horn rule: {?X your:isBrotherOf ?Y} => {?Y your:isBrotherOf ?X}
# BFP sub-goal:  ASK { eg:joe your:isBrotherOf eg:bob } → true in EDB → goal proved
# CONSTRUCT materialises the BFP-derived entailment:
CONSTRUCT { eg:bob your:isBrotherOf eg:joe . }
WHERE {
  GRAPH <https://linkeddata.uriburner.com/DAV/demos/daas/fuxi-semantic-web-reasoner-meshup-claude_sonnet4-1.ttl> {
    eg:joe your:isBrotherOf eg:bob .
    your:isBrotherOf owl:inverseOf your:isBrotherOf .
  }
}

The article shows FuXi using SELECT ?brother { eg:bob your:isBrotherOf ?brother } to demonstrate Sideways Information Passing (SIP): eg:bob is bound (b), ?brother is free (f). FuXi propagates the binding of eg:bob through the BFP meta-interpretation rules, adorning them as isBrotherOf_bf(?X ?_:3) :- hasBrother(?_:3 ?X). This SELECT against the named graph retrieves the entailed value of ?brother.

Sample Dataset (FuXi test suite ↗):

inverseOf ABox:

@prefix your: <http://example.net/vocab#> .
@prefix eg:   <http://example.net/> .

eg:joe your:isBrotherOf eg:bob .   # ABox fact

SIP adornment (from fuxi.owl --output adornment) (TBox — ontology axioms):

# SIP adornments: b=bound, f=free
# Forall ?X ?_:3 ( :isBrotherOf_bf(?X ?_:3) :- your:isBrotherOf(?_:3 ?X) )
# Forall ?X ?_:4 ( :isBrotherOf_bf(?X ?_:4) :- your:isBrotherOf(?_:4 ?X) )
#
# fuxi.owl --method=bfp --dlp --hybrid
#   --why "SELECT ?brother {{ eg:bob your:isBrotherOf ?brother }}"
#   --output adornment test/OWL/inverseOf/premises001.rdf

⇒ ?brother = eg:joe ← BFP with SIP passes bound binding for eg:bob to derive the free ?brother

SPARQL expressing this entailment (click ▶ to run live):

PREFIX your: <http://example.net/vocab#>
PREFIX eg:   <http://example.net/>

# SIP SELECT: eg:bob is bound (b), ?brother is free (f)
# FuXi adorns BFP rules as isBrotherOf_bf and propagates the eg:bob binding
# to efficiently derive ?brother = eg:joe without full table scan
SELECT ?brother
WHERE {
  GRAPH <https://linkeddata.uriburner.com/DAV/demos/daas/fuxi-semantic-web-reasoner-meshup-claude_sonnet4-1.ttl> {
    eg:joe your:isBrotherOf eg:bob .
    eg:bob ?p ?brother .
    FILTER(?p = your:isBrotherOf && ?brother != eg:bob)
  }
}

SPARQL Interlocution is FuXi's mechanism for dispatching SPARQL sub-queries to the EDB during BFP backward-chaining. Before applying Horn rules for OWL functional or inverse-functional properties, FuXi generates and dispatches this ASK to the EDB. If the EDB returns false (no such properties exist), those Horn rules are skipped — a key memoization optimisation described in the article as "complete, sound, and safe memoization even when the rules are recursive."

Sample Dataset (FuXi test suite ↗):

intersectionOf ABox+TBox:

@prefix first: <http://www.w3.org/2002/03owlt/intersectionOf/premises001#> .
@prefix owl:  <http://www.w3.org/2002/07/owl#> .

first:C owl:intersectionOf ( first:Employee first:Student ) .
first:B owl:intersectionOf ( first:Student  first:Employee ) .
first:John a first:B .

⇒ ASK → false ← no functional/inverse-functional properties in EDB → BFP skips those Horn rules (memoisation)

SPARQL expressing this entailment (click ▶ to run live):

PREFIX owl: <http://www.w3.org/2002/07/owl#>

# FuXi generates and dispatches this ASK to the EDB during SPARQL Interlocution
# before deciding whether to apply Functional/InverseFunctional Horn rules
ASK {
  [] a ?KIND
  FILTER(
    ?KIND = owl:InverseFunctionalProperty ||
    ?KIND = owl:FunctionalProperty
  )
}

FuXi's RETE-UL forward-chaining network compiles the TBox axiom exterms:has_brother rdfs:subPropertyOf exterms:has_sibling into a Horn rule and fires it over the ABox. The Doorenbos RETE-UL algorithm (3-tuple facts matching RDF triples) derives and materialises exind:john exterms:has_sibling exind:jack in the named graph. This SELECT retrieves that RETE-UL-derived triple.

Sample Dataset (FuXi test suite ↗):

Superproperty ABox:

@prefix exterms: <http://example.org/terms/> .
@prefix exind:   <http://example.org/> .

exind:john exterms:has_brother exind:jack .
exind:jack exterms:brother     exind:john .

Superproperty TBox (TBox — ontology axioms):

@prefix exterms: <http://example.org/terms/> .
@prefix rdfs: <http://www.w3.org/2000/01/rdf-schema#> .
@prefix owl:  <http://www.w3.org/2002/07/owl#> .

exterms:has_brother rdfs:subPropertyOf exterms:has_sibling .
exterms:brother owl:equivalentProperty exterms:has_brother .

⇒ exind:john exterms:has_sibling exind:jack ← RETE-UL fires subPropertyOf Horn rule, triple materialised in named graph

SPARQL expressing this entailment (click ▶ to run live):

PREFIX exterms: <http://example.org/terms/>

# RETE-UL fires: john has_brother jack + has_brother subPropertyOf has_sibling
# → derives and materialises: john has_sibling jack  (stored in named graph)
SELECT ?subject ?object
WHERE {
  GRAPH <https://linkeddata.uriburner.com/DAV/demos/daas/fuxi-semantic-web-reasoner-meshup-claude_sonnet4-1.ttl> {
    ?subject exterms:has_sibling ?object .
  }
}

FuXi RETE-UL applies both rdfs:subPropertyOf and owl:equivalentProperty Horn rules in one forward-chaining pass, producing the complete deductive closure. This SELECT retrieves all triples in the named graph with subject and predicate from the example namespace — the two ABox facts and every RETE-UL-entailed triple — showing the full closure FuXi computes.

Sample Dataset (FuXi test suite ↗):

Superproperty ABox + RETE-UL closure:

# ABox facts:
exind:john exterms:has_brother exind:jack
exind:jack exterms:brother     exind:john
# RETE-UL entailed (rdfs:subPropertyOf):
exind:john exterms:has_sibling exind:jack

Superproperty TBox (TBox — ontology axioms):

exterms:has_brother rdfs:subPropertyOf exterms:has_sibling .
exterms:brother owl:equivalentProperty exterms:has_brother .

⇒ Full RETE-UL closure: both ABox facts + all derived triples across subPropertyOf and equivalentProperty chains

SPARQL expressing this entailment (click ▶ to run live):

PREFIX exterms: <http://example.org/terms/>
PREFIX exind:   <http://example.org/>

# Full RETE-UL closure over the superproperty dataset
# Returns: john has_brother jack (ABox)
#          jack brother      john (ABox)
#          john has_sibling  jack (RETE-UL: subPropertyOf entailment)
SELECT ?subject ?predicate ?object
WHERE {
  GRAPH <https://linkeddata.uriburner.com/DAV/demos/daas/fuxi-semantic-web-reasoner-meshup-claude_sonnet4-1.ttl> {
    ?subject ?predicate ?object .
    FILTER(
      STRSTARTS(STR(?subject),   'http://example.org/') &&
      STRSTARTS(STR(?predicate), 'http://example.org/terms/')
    )
  }
}
ORDER BY ?subject ?predicate

FuXi BFP reasons over owl:intersectionOf: first:B owl:intersectionOf (first:Student first:Employee) means every member of first:B is simultaneously a Student and an Employee. Given first:John a first:B, BFP derives the class membership entailments. This SELECT retrieves the class assertions from the dataset that BFP reasons over, and the EDB ASK (example 3) is dispatched by FuXi during this same BFP evaluation.

Sample Dataset (FuXi test suite ↗):

intersectionOf ABox+TBox:

@prefix first: <http://www.w3.org/2002/03owlt/intersectionOf/premises001#> .
@prefix owl:  <http://www.w3.org/2002/07/owl#> .

# ABox
first:John a first:B .
# TBox
first:B owl:intersectionOf ( first:Student  first:Employee ) .
first:C owl:intersectionOf ( first:Employee first:Student  ) .

⇒ first:John a first:Student, first:Employee ← BFP derives class memberships via owl:intersectionOf

SPARQL expressing this entailment (click ▶ to run live):

PREFIX first: <http://www.w3.org/2002/03owlt/intersectionOf/premises001#>
PREFIX rdf:   <http://www.w3.org/1999/02/22-rdf-syntax-ns#>

# BFP: John a B + B intersectionOf(Student,Employee) → John a Student, John a Employee
# This SELECT retrieves all class assertions from the intersectionOf dataset
SELECT ?individual ?class
WHERE {
  GRAPH <https://linkeddata.uriburner.com/DAV/demos/daas/fuxi-semantic-web-reasoner-meshup-claude_sonnet4-1.ttl> {
    ?individual rdf:type ?class .
    FILTER(STRSTARTS(STR(?individual), 'http://www.w3.org/2002/03owlt/'))
  }
}