RPI Tetherless World Constellation & IBM Research

SQuARE Reasoning Engine

A revolutionary paradigm for Web Ontology Language (OWL) Description Logic (DL) inferencing: executing deductive reasoning and paraconsistent inconsistency tolerance via declarative SPARQL CONSTRUCT query micro-agents.

Launch Interactive Axiom Reasoner Explore SETS Knowledge Graph

The SQuARE Paradigm: Decoupled Deductive Inferencing 🔗

Transforming monolithic tableau algorithms into lightweight, auditable, and distributed SPARQL 1.1 query agents.

⚡

SPARQL CONSTRUCT Rules

Every OWL DL axiom (Class Disjointness, Transitivity, Property Chains, Subsumption) is encoded as a declarative SPARQL CONSTRUCT query where graph pattern matches form premises and constructed graphs materialize entailments.

🛡️

Inconsistency Resilience

Traditional tableau reasoners suffer complete proof collapse upon detecting contradictions (ex falso quodlibet). SQuARE isolates conflicting individuals into owl:Nothing without corrupting parallel derivations.

🔍

Transparent Explainability

Because each inference is a query execution with explicit variable bindings, reasoning trails are directly inspectable, provable via W3C PROV-O, and reversible through companion Backtracer Agents.

SQuARE Interactive Query Workbench & Axiom Simulator 🔗

Select any OWL DL axiom from the SQuARE Evaluation Test Set (SETS) catalog. Inspect its formal Description Logic formula, underlying instance dataset, and SPARQL CONSTRUCT rule, then execute the inference in real-time.

💡
Plain English Explainer: What's Being Tested?
Demystifying the formal logic for beginners while providing precise semantic mechanics for engineers
🌱 Real-World Intuition & Scenario

Loading scenario...

❓ What We Want to Prove

Loading question...

⚙️ How the SPARQL Rule Works

Loading mechanism...

🚀 Why This Matters in Practice

Loading takeaway...

Select Axiom:
Run on URIBurner
Description Logic Formal Axiom cax-dw
C_1 ⊓ C_2 ⊑ ⊥
Explanation of the axiom and reasoner behavior...
Underlying TBox Schema & ABox Instance Graph
SPARQL CONSTRUCT Inference Rule
Materialized Deductive Entailments Ready

Reasoning Architecture Comparison Matrix 🔗

Comparing SQuARE SPARQL CONSTRUCT Micro-Agents against Traditional Tableau DL Reasoners, Forward Rule Engines, and Neurosymbolic LLMs.

Evaluation Dimension SQuARE (SPARQL Agents) Tableau (HermiT / Pellet) Rule Engines (Virtuoso / Jena) Neurosymbolic LLM Clients
Core Reasoning Mechanism Declarative SPARQL 1.1 CONSTRUCT pattern matching micro-agents Refutation-based semantic tableau state-space search Forward-chaining RETE/SPIN materialization & backward chaining Probabilistic vector attention with hybrid SPARQL grounding
Inconsistency Resilience Paraconsistent & Isolated: Inconsistencies entail typed owl:Nothing without global collapse Non-resilient: Single contradiction causes immediate total proof collapse (ex falso quodlibet) Partial: Handled through explicit negation/filter guards; may fail silently Prone to hallucination: Merges contradictory context unless explicitly validated
Explainability & Traceability Full Step Provenance: Inferences trace back to discrete SPARQL variable bindings & Backtracer Complex, opaque branch-saturation proof trees difficult for non-logicians Rule-level trace logs available via engine debug modes Latent activation weights; requires external ontological guardrails
Scalability & DB Integration Native Database Execution: Runs directly inside disk-backed triplestores (Virtuoso, Jena) Requires in-memory graph loading; exponential worst-case on large ABoxes High scalability with native columnar and quad-store indexing Bounded by context window size and API latency
Rule Customizability Modular Micro-Rules: Easily toggle individual DL axioms or add domain-specific queries Monolithic engine configuration; axiom sets fixed by DL profile Custom rules supported via vendor-specific rule languages or SPIN Customizable via prompt instructions, fine-tuning, and tool use
Distributed & Federated Execution Federated SPARQL (SERVICE): Rules execute asynchronously across decentralized endpoints Centralized single-node computation required for tableau closure Database-level clustering or distributed SPARQL endpoints API-based agent swarms with tool-calling capabilities
Open Standards Compliance 100% W3C SPARQL 1.1, Turtle, OWL 2, W3C PROV-O W3C OWL 2 Direct Semantics & DIG interface W3C SPARQL, RIF, SPIN, or proprietary rule syntax Proprietary vendor APIs with JSON-LD / schema.org tooling

SQuARE Deductive Inference Execution Pipeline 🔗

The 7-step engineering procedure for executing and validating OWL DL reasoning via SPARQL micro-agents.

1

Ingest TBox Schema and ABox Instance Knowledge Graph

Load the target OWL ontology schema (TBox) and instance triples (ABox) into an RDF store or local graph model (such as OpenLink Virtuoso or RDFLib).

2

Select Target OWL DL Axiom Rule from SQuARE Catalog

Identify the required DL inference rule (e.g., Class Disjointness, Transitivity, Property Chains, or Subsumption) based on the deductive query goal.

3

Formulate SPARQL CONSTRUCT Query Mapping DL Premise to Graph Pattern

Translate the DL axiom antecedent into the WHERE clause graph pattern and the consequent into the CONSTRUCT clause template.

4

Execute SPARQL CONSTRUCT Query against Target RDF Graph

Run the declarative query against the SPARQL 1.1 protocol endpoint to generate the inferred triple graph in a single execution step.

5

Detect and Isolate Inconsistencies (owl:Nothing Entailments)

Inspect the result graph for ?resource rdf:type owl:Nothing triples. If found, isolate the inconsistent individual without triggering proof collapse.

6

Materialize Inferred Triples or Route to Deductive Backtracer Agent

Merge consistent inferred triples into the working knowledge graph or pass the entailment trail to a SQuARE Backtracer Agent for proof explainability.

7

Verify Reasoning Provenance and Publish Inferred Knowledge

Attach W3C PROV-O metadata linking inferred assertions back to the executing SPARQL agent, rule identifier, and source premise triples.

Frequently Asked Questions (FAQ) 🔗

Key questions on SQuARE's deductive reasoning architecture, paraconsistent logic, and SPARQL 1.1 query mechanics.

How does SQuARE implement OWL DL reasoning using SPARQL CONSTRUCT?
SQuARE translates formal Description Logic (DL) inference rules directly into declarative SPARQL CONSTRUCT queries. The antecedent (premise) of the DL axiom is mapped to the SPARQL WHERE clause pattern, and the consequent (conclusion) is materialized via the CONSTRUCT clause template, executing deductive inferencing natively within any standard SPARQL 1.1 store.
Why is SPARQL CONSTRUCT inference particularly effective for Class Disjointness?
In classical tableau reasoners, discovering an instance of disjoint classes causes the entire knowledge base to become inconsistent, triggering an explosive collapse where anything can be derived (ex falso quodlibet). SQuARE isolates the contradiction by constructing an explicit assertion '?resource rdf:type owl:Nothing', allowing reasoning over remaining consistent facts to proceed unimpeded.
How does SQuARE handle inconsistencies without catastrophic proof explosion?
Because SQuARE uses query-driven micro-agents executing discrete CONSTRUCT rules rather than an monolithic global tableau tableau saturation, an inconsistency in one domain concept (such as sets-kb:ImaginaryFriend being typed as both Real and Fictional) is localized to a specific typed violation without corrupting unrelated inference paths across the graph.
What is SETS and how does it evaluate DL reasoning complexity?
SETS (SQuARE Evaluation Test Set) is an extensible benchmark ontology and dataset leveraging the Semanticscience Integrated Ontology (SIO). It provides isolated, per-axiom test cases for every OWL DL construct, allowing practitioners to audit the specific DL complexity tier and axiom coverage supported by any RDF reasoner or triplestore.
What is the difference between SQuARE and tableau-based reasoners like HermiT or Pellet?
Tableau reasoners (HermiT, Pellet, FaCT++) use refutation-based model construction algorithms that require loading the entire ontology into memory and suffer exponential worst-case complexity on expressive DL profiles. SQuARE is a forward-chaining, pattern-directed engine that operates directly against live databases using standard query engines, scaling to billions of triples.
How does property chain inclusion (prp-spo2) translate into SPARQL path patterns?
Property chain axioms (such as overlapsWith ∘ isPartOf ⊑ overlapsWith) are translated into SPARQL join patterns that traverse rdf:first and rdf:rest/rdf:first list structures in the TBox to dynamically bind ?prop1 and ?prop2, chaining them across intermediate nodes (?x ?prop1 ?mid . ?mid ?prop2 ?o) to construct the direct composite relationship.
Can SQuARE rules be loaded directly into triple stores like OpenLink Virtuoso or Apache Jena?
Yes. SQuARE's SPARQL CONSTRUCT queries are 100% W3C SPARQL 1.1 compliant. They can be executed directly as scheduled batch inference scripts, wrapped as SPIN (SPARQL Inferencing Notation) rules in Virtuoso, or registered in Apache Jena ARQ inference pipelines for automated forward-chaining materialization.
How does SQuARE address the Open World Assumption (OWA) vs Closed World Assumption (CWA)?
SQuARE preserves the Open World Assumption for monotonic deductive rules (such as subClassOf and property hierarchies), while leveraging SPARQL's scoped Negation as Failure (NOT EXISTS / MINUS) where explicit closed-world checks (such as negative property assertions or missing mandatory attributes) are deliberately required by the application.
What are the explainability advantages of SQuARE's agent-based deductive inference?
Every triple generated by SQuARE carries explicit provenance linking it to the specific SPARQL query template, executing agent ID, and matching premise bindings in the source graph. The companion SQuARE Backtracer Agent can recursively trace any inferred assertion back to its foundational axioms, providing human-readable proof trees.
How does SQuARE support hybrid and distributed reasoning across micro-agents?
Because each DL axiom is encapsulated as a standalone query, SQuARE rules can be distributed across federated SPARQL endpoints using SERVICE clauses. Individual micro-agents can specialize in specific axiom families (e.g., temporal, spatial, or clinical domains) and coordinate asynchronously without central state locks.
How does SQuARE handle complex cardinality and qualified cardinality restrictions?
SQuARE expresses max, min, and exact cardinality restrictions by combining SPARQL aggregation (COUNT(?o) AS ?cnt), GROUP BY ?x, and HAVING filters against owl:maxQualifiedCardinality thresholds, generating inconsistency flags or type assertions when bounds are breached.
How does SQuARE compare with Virtuoso SPIN rules?
Virtuoso SPIN and SQuARE share the same foundational philosophy: using SPARQL as a first-class inference language. While SPIN represents rules as RDF schema metadata attached to class definitions (spin:rule), SQuARE provides an open-source, vendor-agnostic catalog of pure SPARQL 1.1 CONSTRUCT templates validated against the complete OWL 2 DL axiom suite.

Technical Glossary 🔗

Core concepts in Description Logic, Semantic Web standards, and paraconsistent reasoning engines.

Description Logic (DL)
A family of formal knowledge representation languages that provide the theoretical foundation for OWL, equipped with decidable reasoning algorithms.
Deductive Reasoning
A logical process in which a conclusion is drawn from the concord of multiple premises that are assumed to be true, deriving guaranteed entailments.
SPARQL
An RDF query language and W3C standard capable of retrieving, manipulating, and constructing graph data stored in RDF format across endpoints.
Inconsistency-Tolerant Reasoning
A paraconsistent reasoning capability that allows an inference engine to derive meaningful conclusions from contradictory knowledge without collapsing into triviality.
SIO Ontology
An upper-level ontology facilitating biomedical knowledge representation and data integration, serving as the foundational schema for SETS test cases.
Transitive Property
A binary relation R over a set where for all x, y, z, if x R y and y R z hold, then x R z necessarily holds.
Subsumption (Class Inclusion)
A hierarchical relation between concepts where every instance of a sub-concept is logically guaranteed to be an instance of the super-concept.
Equivalence Relation
A binary relation that is reflexive, symmetric, and transitive, asserting identical semantic extension between classes or properties.
Reflexive Property
A relation where every individual is related to itself (x R x) for all elements in the domain of discourse.
Irreflexive Property
A relation where no individual can be related to itself (NOT(x R x)), triggering an inconsistency if self-reference occurs.
Symmetric Property
A relation where if x R y holds, then y R x is necessarily true.
OWL 2
A W3C standard ontology language designed to represent rich and complex knowledge about things and relations with formal semantics.
Knowledge Graph
A knowledge base that uses a graph-structured data model to integrate, process, and extract value from interconnected real-world entities.
Inference Engine
A software component that applies logical rules to a knowledge base to deduce new information and test consistency.

SETS & SQuARE Knowledge Graph Explorer 🔗

Interactive force-directed graph visualization of the SQuARE axioms, SIO ontology classes, SETS individuals, and materialized deductive entailments.

Graph Filters 31 Nodes | 27 Edges
💡 Drag nodes to pin position. Double-click to unpin. Click node labels to explore via URIBurner.

SPARQL Query Recipes & Live Endpoint Execution 🔗

Pre-formulated W3C SPARQL 1.1 queries for inspecting, validating, and reasoning over the SQuARE knowledge base on live Virtuoso endpoints scoped to the DAV named graph https://linkeddata.uriburner.com/DAV/demos/daas/square-sparql-agent-reasoning-axioms-gemini_3_7_flash-1.ttl.

1. Class Disjointness Inconsistency Audit (CONSTRUCT) CONSTRUCT
💡 Plain English Breakdown (Novice & Expert)

What's Being Tested: Checks whether any entity is mistakenly declared as both sio:Real and sio:Fictional (mutually exclusive concepts).

How the Query Solves It: Scans the graph for any resource with two classes linked by owl:disjointWith. It constructs a localized assertion ?resource rdf:type owl:Nothing to isolate the error without triggering a system crash.

PREFIX rdf: <http://www.w3.org/1999/02/22-rdf-syntax-ns#>
PREFIX owl: <http://www.w3.org/2002/07/owl#>
PREFIX sets-kb: <http://purl.org/ontology/sets/kb#>
PREFIX sets: <http://purl.org/ontology/sets/ont#>
PREFIX sio: <http://semanticscience.org/resource/>

CONSTRUCT {
  ?resource rdf:type owl:Nothing .
}
FROM <https://linkeddata.uriburner.com/DAV/demos/daas/square-sparql-agent-reasoning-axioms-gemini_3_7_flash-1.ttl>
WHERE {
  ?resource rdf:type ?class .
  ?resource rdf:type ?disjointClass .
  { ?class owl:disjointWith ?disjointClass . } 
    UNION
  { ?disjointClass owl:disjointWith ?class . }
}
Target Named Graph: SQuARE SETS Run on URIBurner
2. Transitive Part-Whole (Mereology) Path Deduction (CONSTRUCT) CONSTRUCT
💡 Plain English Breakdown (Novice & Expert)

What's Being Tested: Multi-hop anatomy reasoning: if Fingernail isPartOf Finger and Finger isPartOf Hand, is the fingernail part of the hand?

How the Query Solves It: Matches the transitive property sio:isPartOf across intermediate nodes (?x -> ?y -> ?z) and materializes the direct edge Fingernail isPartOf Hand.

PREFIX rdf: <http://www.w3.org/1999/02/22-rdf-syntax-ns#>
PREFIX owl: <http://www.w3.org/2002/07/owl#>
PREFIX sets-kb: <http://purl.org/ontology/sets/kb#>
PREFIX sets: <http://purl.org/ontology/sets/ont#>
PREFIX sio: <http://semanticscience.org/resource/>

CONSTRUCT {
  ?x ?p ?z .
}
FROM <https://linkeddata.uriburner.com/DAV/demos/daas/square-sparql-agent-reasoning-axioms-gemini_3_7_flash-1.ttl>
WHERE {
  ?x ?p ?y .
  ?y ?p ?z .
  ?p rdf:type owl:ObjectProperty , owl:TransitiveProperty .
}
Target Named Graph: SQuARE SETS Run on URIBurner
3. SIO Subsumption Hierarchy Traversal (SELECT) SELECT
💡 Plain English Breakdown (Novice & Expert)

What's Being Tested: Taxonomical inheritance: listing every sub-class and all of its ancestor categories across the entire SIO ontology hierarchy.

How the Query Solves It: Uses the property path rdfs:subClassOf+ to traverse arbitrary depths of the classification tree in a single query.

PREFIX rdfs: <http://www.w3.org/2000/01/rdf-schema#>
PREFIX owl: <http://www.w3.org/2002/07/owl#>
PREFIX sio: <http://semanticscience.org/resource/>

SELECT DISTINCT ?subClass ?superClass
FROM <https://linkeddata.uriburner.com/DAV/demos/daas/square-sparql-agent-reasoning-axioms-gemini_3_7_flash-1.ttl>
WHERE {
  ?subClass rdfs:subClassOf+ ?superClass .
  FILTER(?subClass != ?superClass)
}
ORDER BY ?superClass ?subClass
Target Named Graph: SQuARE SETS Run on URIBurner