{
"path": "/3m6pxnnhrys2p",
"site": "at://did:plc:p7sxjpo2opcfkn7cgi5jqyqi/site.standard.publication/3m6ol2sdsnc2r",
"$type": "site.standard.document",
"title": "Open World vs Closed World: Modeling OWL and SHACL Semantics in Agda",
"content": {
"$type": "pub.leaflet.content",
"pages": [
{
"id": "019acc91-c5f6-7bba-aef1-89220ef2885d",
"$type": "pub.leaflet.pages.linearDocument",
"blocks": [
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": "The tension between the Open World Assumption (OWA) and Closed World Assumption (CWA) represents one of the fundamental philosophical and practical divides in knowledge representation. OWL (Web Ontology Language) embraces OWA, treating absence of information as unknown rather than false. SHACL (Shapes Constraint Language), conversely, validates data under CWA, where what is not explicitly stated is considered false. This article explores how dependent type theory, specifically Agda, can model both approaches and potentially bridge this conceptual gap."
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.header",
"level": 2,
"facets": [],
"plaintext": "Open World Assumption (OWA)"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [
{
"index": {
"byteEnd": 140,
"byteStart": 133
},
"features": [
{
"$type": "pub.leaflet.richtext.facet#italic"
}
]
}
],
"plaintext": "Under OWA, the world is inherently incomplete. If we cannot prove a statement is true, we cannot conclude it is false — it remains unknown. This assumption aligns with the reality of distributed, evolving knowledge systems where information is constantly being discovered and added."
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [
{
"index": {
"byteEnd": 8,
"byteStart": 0
},
"features": [
{
"$type": "pub.leaflet.richtext.facet#bold"
}
]
},
{
"index": {
"byteEnd": 94,
"byteStart": 91
},
"features": [
{
"$type": "pub.leaflet.richtext.facet#italic"
}
]
}
],
"plaintext": "Example: If we have no statement that “Alice knows Bob,” we cannot conclude Alice does not know Bob. The information is simply absent."
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.header",
"level": 2,
"facets": [],
"plaintext": "Closed World Assumption (CWA)"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": "Under CWA, what is not known to be true is considered false. This assumption works well for validation, databases, and bounded domains where we have complete information."
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [
{
"index": {
"byteEnd": 8,
"byteStart": 0
},
"features": [
{
"$type": "pub.leaflet.richtext.facet#bold"
}
]
}
],
"plaintext": "Example: If our database has no record of “Alice knows Bob,” we can definitively say this relationship does not exist in our system."
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.header",
"level": 2,
"facets": [],
"plaintext": "OWL and the Open World"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": "OWL’s reasoning is built on description logic, which operates under OWA. This has profound implications:"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": ":Alice a :Person ."
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": ":Bob a :Person ."
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": "# Ontology constraint"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": ":Person owl:equivalentClass ["
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": "a owl:Restriction ;"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": "owl:onProperty :hasParent ;"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": "owl:minCardinality 2"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": "] ."
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [
{
"index": {
"byteEnd": 92,
"byteStart": 89
},
"features": [
{
"$type": "pub.leaflet.richtext.facet#italic"
}
]
}
],
"plaintext": "In this example, even though we haven’t stated Alice’s parents, an OWL reasoner will not conclude Alice violates the constraint. The information about Alice’s parents is simply unknown — she might have parents that haven’t been stated yet."
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.header",
"level": 2,
"facets": [],
"plaintext": "SHACL and the Closed World"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": "SHACL validates RDF graphs under CWA, making it perfect for data quality checking:"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": "# SHACL Shape"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": ":PersonShape a sh:NodeShape ;"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": "sh:targetClass :Person ;"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": "sh:property ["
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.code",
"language": "plaintext",
"plaintext": "sh:path :hasParent ; \n\nsh:minCount 2 ; \n\nsh:message \"A person must have at least 2 parents declared\" \n"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": "] ."
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": "When validating Alice’s data against this shape, SHACL will report a violation because only the stated parents are considered — absence means nonexistence."
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.header",
"level": 2,
"facets": [],
"plaintext": "Modeling in Agda: Type-Theoretic Foundations"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": "Agda’s dependent types provide a rigorous foundation for modeling both assumptions. The key insight is that OWA corresponds to intuitionistic logic (where absence of proof ≠ proof of absence), while CWA corresponds to classical logic with decidability."
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.header",
"level": 2,
"facets": [],
"plaintext": "Core Definitions"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": "module WorldAssumptions where"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": "open import Data.Bool using (Bool; true; false)"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": "open import Data.Maybe using (Maybe; just; nothing)"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": "open import Data.Nat using (ℕ; zero; suc; _+_; _≤_)"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": "open import Relation.Nullary using (¬_; Dec; yes; no)"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": "open import Relation.Binary.PropositionalEquality using (_≡_; refl)-- A universe of entities"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": "postulate Entity : Set-- Properties as relations between entities"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": "postulate Property : Entity → Entity → Set"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.header",
"level": 2,
"facets": [],
"plaintext": "Open World Assumption: OWL-like Agda"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [
{
"index": {
"byteEnd": 58,
"byteStart": 41
},
"features": [
{
"$type": "pub.leaflet.richtext.facet#italic"
}
]
}
],
"plaintext": "In the open world, we model knowledge as what we can prove, not what we can disprove:"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": "module OpenWorld where"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": "open import Data.List using (List; []; _∷_; any)"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": "open import Data.Product using (_×_; ∃; _,_; proj₁; proj₂)"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": "record KnowledgeBase : Set₁ where"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.code",
"language": "plaintext",
"plaintext": "field \n\n facts : List (∃ λ (subject : Entity) → ∃ λ (object : Entity) → Property subject object)\n\n\n \n"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": "data OWAValue : Set where"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.code",
"language": "plaintext",
"plaintext": "known-true : OWAValue \n\nknown-false : OWAValue \n\nunknown : OWAValue\n\n\n \n\n"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": "query : KnowledgeBase → Entity → Entity → Property → OWAValue"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": "query kb subject object prop ="
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.code",
"language": "plaintext",
"plaintext": "if any (matches subject object prop) (KnowledgeBase.facts kb) \n\nthen known-true \n\nelse unknown \n\n\n \n"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": "record OntologyClass : Set₁ where"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.code",
"language": "plaintext",
"plaintext": "field \n\n name : String \n\n \n\n \n\n necessaryConditions : Entity → Set \n\n \n\n checkSatisfiable : (e : Entity) → (kb : KnowledgeBase) → \n\n Maybe (necessaryConditions e)\n\n\n \n"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": "Person : OntologyClass"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": "Person = record"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.code",
"language": "plaintext",
"plaintext": "{ name = \"Person\" \n\n; necessaryConditions = λ e → \n\n ∃ λ (p1 : Entity) → ∃ λ (p2 : Entity) → \n\n (Property e p1 × Property e p2 × ¬ (p1 ≡ p2)) \n\n; checkSatisfiable = λ e kb → \n\n \n\n \n\n findParents e kb \n\n}\n\n\n \n\n"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": "deriveNewFacts : KnowledgeBase → List Inference → KnowledgeBase"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": "deriveNewFacts kb rules ="
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.code",
"language": "plaintext",
"plaintext": "applyInferences kb rules\n\n\n \n"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": "data QueryResult : Set where"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.code",
"language": "plaintext",
"plaintext": "definitely-true : QueryResult \n\ndefinitely-false : QueryResult \n\ninsufficient-data : QueryResult \n\n\nopenWorldQuery : KnowledgeBase → Entity → Property → Entity → QueryResult \n"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": "openWorldQuery kb subj prop obj ="
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.code",
"language": "plaintext",
"plaintext": "case lookup kb subj prop obj of \n\n found-true → definitely-true \n\n found-false → definitely-false \n\n not\\-found → insufficient-data \n"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.header",
"level": 2,
"facets": [],
"plaintext": "Closed World Assumption: SHACL-like Agda"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": "In the closed world, we can definitively determine truth values based on what’s present:"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": "module ClosedWorld where"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": "open import Data.List using (List; []; _∷_; length; filter)"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": "open import Data.Nat using (ℕ; _≤?_)"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": "open import Data.Product using (_×_; ∃; _,_)"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": "open import Relation.Nullary using (Dec; yes; no)"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": "record DataGraph : Set₁ where"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.code",
"language": "plaintext",
"plaintext": "field \n\n entities : List Entity \n\n triples : List (Entity × Property × Entity) \n\n \n\n complete : Bool \n\n\n \n"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": "data CWAValue : Set where"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.code",
"language": "plaintext",
"plaintext": "true : CWAValue \n\nfalse : CWAValue\n\n\n \n"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": "query : DataGraph → Entity → Property → Entity → CWAValue"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": "query dg subject prop object ="
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.code",
"language": "plaintext",
"plaintext": "if (subject , prop , object) ∈ DataGraph.triples dg \n\nthen true \n\nelse false \n\n\n \n"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": "record Shape : Set₁ where"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.code",
"language": "plaintext",
"plaintext": "field \n\n targetClass : Entity → Bool \n\n \n\n \n\n constraints : List (Entity → DataGraph → Bool)\n\n\n \n"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": "data ValidationResult : Set where"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.code",
"language": "plaintext",
"plaintext": "conforms : ValidationResult \n\nviolates : List String → ValidationResult \n\n\n \n"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": "PersonShape : Shape"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": "PersonShape = record"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.code",
"language": "plaintext",
"plaintext": "{ targetClass = isPersonClass \n\n; constraints = hasMinParents 2 ∷ \\[\\] \n\n} \n\nwhere \n\n hasMinParents : ℕ → Entity → DataGraph → Bool \n\n hasMinParents n entity dg = \n\n let parents = countParents entity dg \n\n in n ≤? parents\n\n\n countParents : Entity → DataGraph → ℕ \n\n countParents entity dg = \n\n length (filter (isParentTriple entity) (DataGraph.triples dg))\n\n\n \n"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": "validate : DataGraph → Shape → Entity → ValidationResult"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": "validate dg shape entity ="
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.code",
"language": "plaintext",
"plaintext": "if all (λ constraint → constraint entity dg) (Shape.constraints shape) \n\nthen conforms \n\nelse violates (collectErrors dg shape entity)\n\n\n \n"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": "isValid : DataGraph → Shape → Entity → Dec (ValidationResult ≡ conforms)"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": "isValid dg shape entity ="
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.code",
"language": "plaintext",
"plaintext": "case validate dg shape entity of \n\n conforms → yes refl \n\n violates \\_ → no (λ ())\n"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.header",
"level": 2,
"facets": [],
"plaintext": "Bridging the Gap: Hybrid Approach"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": "The most powerful approach combines both paradigms:"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": "module HybridWorld where"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": "open OpenWorld using (KnowledgeBase; OWAValue)"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": "open ClosedWorld using (DataGraph; ValidationResult)"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.code",
"language": "plaintext",
"plaintext": "record HybridKnowledgeSystem : Set₁ where \n\nfield \n\n \n\n ontology : KnowledgeBase \n\n inferenceRules : List InferenceRule\n\n\n \n\n instanceData : DataGraph \n\n validationShapes : List Shape\n\n\n \n\n enrichData : DataGraph → KnowledgeBase → DataGraph\n\n\n \n"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": "validateWithReasoning : HybridKnowledgeSystem → Entity → ValidationResult"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": "validateWithReasoning hks entity ="
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.code",
"language": "plaintext",
"plaintext": "let enrichedData \\= HybridKnowledgeSystem.enrichData hks \n\n (HybridKnowledgeSystem.instanceData hks) \n\n (HybridKnowledgeSystem.ontology hks) \n\nin ClosedWorld.validate enrichedData shape entity \n\nwhere \n\n shape \\= head (HybridKnowledgeSystem.validationShapes hks)\n\n\n \n"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": "inferThenValidate : KnowledgeBase → DataGraph → Shape → Entity → ValidationResult"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": "inferThenValidate onto data shape entity ="
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.code",
"language": "plaintext",
"plaintext": "let derived \\= deriveFromOntology onto data \n\n \n\n complete \\= mergeInferred data derived \n\n \n\nin ClosedWorld.validate complete shape entity\n"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.header",
"level": 2,
"facets": [],
"plaintext": "Practical Example: Family Relationships"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": "Let’s model a concrete example with both approaches:"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": "module FamilyExample where"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": "open import Data.String using (String)"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.code",
"language": "plaintext",
"plaintext": "\\-- Entities \n"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": "postulate"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.code",
"language": "plaintext",
"plaintext": "alice bob charlie diana : Entity\n\n\n\\-- Properties \n"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": "postulate"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.code",
"language": "plaintext",
"plaintext": "hasParent : Property \n\nhasSibling : Property\n\n\n\\-- OWL-like ontology (OWA) \n"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": "familyOntology : OpenWorld.KnowledgeBase"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": "familyOntology = record"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.code",
"language": "plaintext",
"plaintext": "{ facts \\= \n\n (alice , (bob , hasParent)) ∷ \n\n (alice , (charlie , hasParent)) ∷ \n\n \\[\\] \n\n}\n\n\n\\-- Question: Does Diana have parents? \n"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": "queryDiana : OpenWorld.OWAValue"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": "queryDiana = OpenWorld.query familyOntology diana anyEntity hasParent"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": "-- Result: unknown (not false!)"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.code",
"language": "plaintext",
"plaintext": "\\-- SHACL-like validation (CWA) \n"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": "familyData : ClosedWorld.DataGraph"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": "familyData = record"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.code",
"language": "plaintext",
"plaintext": "{ entities \\= alice ∷ bob ∷ charlie ∷ diana ∷ \\[\\] \n\n; triples \\= \n\n (alice , hasParent , bob) ∷ \n\n (alice , hasParent , charlie) ∷ \n\n \\[\\] \n\n; complete \\= true \n\n}\n\n\npersonShape : ClosedWorld.Shape \n"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": "personShape = record"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.code",
"language": "plaintext",
"plaintext": "{ targetClass \\= λ \\_ → true \n\n; constraints \\= requiresExactlyTwoParents ∷ \\[\\] \n\n}\n\n\n\\-- Validation: Does Diana conform? \n"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": "validateDiana : ClosedWorld.ValidationResult"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": "validateDiana = ClosedWorld.validate familyData personShape diana"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": "-- Result: violates [\"Diana has 0 parents, requires 2\"]"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.code",
"language": "plaintext",
"plaintext": "\\-- Key difference: \n"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": "-- - OWA: \"We don't know if Diana has parents\" (unknown)"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": "-- - CWA: \"Diana does NOT have parents\" (false/violation)"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.header",
"level": 2,
"facets": [],
"plaintext": "Advanced: Dependent Types for Schema Evolution"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": "One powerful application of this approach is modeling schema evolution:"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": "module SchemaEvolution where"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": "record EvolvingSchema (version : ℕ) : Set₁ where"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.code",
"language": "plaintext",
"plaintext": "field \n\n classes : List OntologyClass \n\n \n\n backwardCompatible : (v : ℕ) → v ≤ version → \n\n KnowledgeBase → Maybe ValidationResult\n\n\n \n"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": "record ValidationSnapshot (version : ℕ) : Set₁ where"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.code",
"language": "plaintext",
"plaintext": "field \n\n frozenSchema : EvolvingSchema version \n\n dataAtVersion : DataGraph \n\n \n\n mustConform : ClosedWorld.validate dataAtVersion shapes entities ≡ conforms\n"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.header",
"level": 2,
"facets": [],
"plaintext": "Type-Theoretic Insights"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.header",
"level": 2,
"facets": [],
"plaintext": "OWA as Intuitionistic Logic"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": "The OWA naturally corresponds to intuitionistic/constructive logic, where:"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": "data Proof (P : Set) : Set where"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": "evidence : P → Proof P"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": "-- But absence of proof is not proof of absence"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": "-- ¬ (Proof P) does NOT imply Proof (¬ P)-- In Agda, this is natural:"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": "openWorldNegation : {P : Set} → ¬ (Proof P) → Proof (¬ P)"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": "openWorldNegation absence = {!!} -- Cannot be constructed!"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.header",
"level": 2,
"facets": [],
"plaintext": "CWA as Classical Logic with LEM"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": "The CWA essentially adds the Law of Excluded Middle:"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": "postulate"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": "closed-world-LEM : (P : Set) → Dec P"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": "-- This allows definitive validation"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": "closedWorldNegation : {P : Set} → ¬ (Proof P) → Proof (¬ P)"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": "closedWorldNegation {P} absence ="
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": "case closed-world-LEM P of"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.code",
"language": "plaintext",
"plaintext": "yes p → absurd (absence (evidence p)) \n\nno ¬p → evidence ¬p\n"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.header",
"level": 2,
"facets": [],
"plaintext": "Modal Logic Perspective"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": "We can also model the distinction using modal operators:"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": "module ModalPerspective where"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": "-- □P = \"necessarily P\" = proven in ontology (OWA)"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": "-- ◇P = \"possibly P\" = not contradicted (OWA)"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": "-- P = \"actually P\" = present in data (CWA)"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.code",
"language": "plaintext",
"plaintext": "record ModalKnowledge : Set₁ where \n\nfield \n\n necessary : Entity → Property → Entity → Set -- □ \n\n possible : Entity → Property → Entity → Set -- ◇ \n\n actual : Entity → Property → Entity → Bool -- P (decidable)\n\n\n -- Modal axioms \n\n necessary-implies-actual : ∀ {s p o} → necessary s p o → actual s p o ≡ true \n\n actual\\-implies-possible : ∀ {s p o} → actual s p o ≡ true → possible s p o\n"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.header",
"level": 2,
"facets": [],
"plaintext": "Practical Implications"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.header",
"level": 2,
"facets": [],
"plaintext": "When to Use OWA (OWL-like)"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.unorderedList",
"children": [
{
"$type": "pub.leaflet.blocks.unorderedList#listItem",
"content": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": "Integrating data from multiple sources"
},
"children": []
},
{
"$type": "pub.leaflet.blocks.unorderedList#listItem",
"content": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": "Evolving schemas over time"
},
"children": []
},
{
"$type": "pub.leaflet.blocks.unorderedList#listItem",
"content": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": "Reasoning with incomplete information"
},
"children": []
},
{
"$type": "pub.leaflet.blocks.unorderedList#listItem",
"content": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": "Ontology development and knowledge discovery"
},
"children": []
},
{
"$type": "pub.leaflet.blocks.unorderedList#listItem",
"content": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": "Semantic web and linked data scenarios"
},
"children": []
}
]
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.header",
"level": 2,
"facets": [],
"plaintext": "When to Use CWA (SHACL-like)"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.unorderedList",
"children": [
{
"$type": "pub.leaflet.blocks.unorderedList#listItem",
"content": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": "Data quality validation"
},
"children": []
},
{
"$type": "pub.leaflet.blocks.unorderedList#listItem",
"content": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": "Database integrity constraints"
},
"children": []
},
{
"$type": "pub.leaflet.blocks.unorderedList#listItem",
"content": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": "API response validation"
},
"children": []
},
{
"$type": "pub.leaflet.blocks.unorderedList#listItem",
"content": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": "Form validation and user input"
},
"children": []
},
{
"$type": "pub.leaflet.blocks.unorderedList#listItem",
"content": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": "Compliance checking with fixed rules"
},
"children": []
}
]
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.header",
"level": 2,
"facets": [],
"plaintext": "When to Use Hybrid"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.unorderedList",
"children": [
{
"$type": "pub.leaflet.blocks.unorderedList#listItem",
"content": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": "Validate user input (CWA) against a rich domain model (OWA)"
},
"children": []
},
{
"$type": "pub.leaflet.blocks.unorderedList#listItem",
"content": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": "Enrich incomplete data with inferred facts before validation"
},
"children": []
},
{
"$type": "pub.leaflet.blocks.unorderedList#listItem",
"content": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": "Progressive validation: warn vs. error"
},
"children": []
},
{
"$type": "pub.leaflet.blocks.unorderedList#listItem",
"content": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": "Multi-stage pipelines: reason (OWA) then validate (CWA)"
},
"children": []
}
]
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.header",
"level": 2,
"facets": [],
"plaintext": "Conclusion"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": "Modeling OWL’s OWA and SHACL’s CWA in Agda reveals the deep logical and type-theoretic foundations of these approaches. OWA corresponds to intuitionistic logic and proof theory, while CWA assumes decidability and classical reasoning. By implementing both in dependent types, we gain:"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.unorderedList",
"children": [
{
"$type": "pub.leaflet.blocks.unorderedList#listItem",
"content": {
"$type": "pub.leaflet.blocks.text",
"facets": [
{
"index": {
"byteEnd": 16,
"byteStart": 0
},
"features": [
{
"$type": "pub.leaflet.richtext.facet#bold"
}
]
}
],
"plaintext": "Formal precision: Exact specifications of what each assumption means"
},
"children": []
},
{
"$type": "pub.leaflet.blocks.unorderedList#listItem",
"content": {
"$type": "pub.leaflet.blocks.text",
"facets": [
{
"index": {
"byteEnd": 13,
"byteStart": 0
},
"features": [
{
"$type": "pub.leaflet.richtext.facet#bold"
}
]
}
],
"plaintext": "Composability: Ability to mix both approaches as needed"
},
"children": []
},
{
"$type": "pub.leaflet.blocks.unorderedList#listItem",
"content": {
"$type": "pub.leaflet.blocks.text",
"facets": [
{
"index": {
"byteEnd": 11,
"byteStart": 0
},
"features": [
{
"$type": "pub.leaflet.richtext.facet#bold"
}
]
}
],
"plaintext": "Correctness: Type-checked guarantees about reasoning soundness"
},
"children": []
},
{
"$type": "pub.leaflet.blocks.unorderedList#listItem",
"content": {
"$type": "pub.leaflet.blocks.text",
"facets": [
{
"index": {
"byteEnd": 7,
"byteStart": 0
},
"features": [
{
"$type": "pub.leaflet.richtext.facet#bold"
}
]
}
],
"plaintext": "Clarity: Explicit about what we know vs. what we assume"
},
"children": []
}
]
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": "The future of knowledge representation may lie not in choosing one assumption over the other, but in understanding when each applies and how to bridge between them. Dependent type theory provides the rigorous foundation to make this bridge formal, safe, and practical."
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": "To read more :"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [
{
"index": {
"byteEnd": 75,
"byteStart": 0
},
"features": [
{
"uri": "https://leanpub.com/dependenttypesdttlogicholforaiagentreadyknowledgegraphs",
"$type": "pub.leaflet.richtext.facet#link"
}
]
}
],
"plaintext": "https://leanpub.com/dependenttypesdttlogicholforaiagentreadyknowledgegraphs"
}
}
]
}
]
},
"bskyPostRef": {
"cid": "bafyreihqijw7j6rcz6l6g54i35ylwenmelm35j7opmiai4qpncbrntxsya",
"uri": "at://did:plc:p7sxjpo2opcfkn7cgi5jqyqi/app.bsky.feed.post/3m6pxnwwapk2d",
"commit": {
"cid": "bafyreibjrlsktyggkuimceqn3io6dgmp2qxyy4rttryg4d23qaew5ezipi",
"rev": "3m6pxnwzfgu2s"
},
"validationStatus": "valid"
},
"description": "",
"publishedAt": "2025-11-28T22:46:41.879Z"
}