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.

Open World Assumption (OWA)

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.

Example: If we have no statement that “Alice knows Bob,” we cannot conclude Alice does not know Bob. The information is simply absent.

Closed World Assumption (CWA)

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.

Example: If our database has no record of “Alice knows Bob,” we can definitively say this relationship does not exist in our system.

OWL and the Open World

OWL’s reasoning is built on description logic, which operates under OWA. This has profound implications:

:Alice a :Person .

:Bob a :Person .

# Ontology constraint

:Person owl:equivalentClass [

a owl:Restriction ;

owl:onProperty :hasParent ;

owl:minCardinality 2

] .

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.

SHACL and the Closed World

SHACL validates RDF graphs under CWA, making it perfect for data quality checking:

# SHACL Shape

:PersonShape a sh:NodeShape ;

sh:targetClass :Person ;

sh:property [

sh:path :hasParent ;  

sh:minCount 2 ;  

sh:message "A person must have at least 2 parents declared"  

] .

When validating Alice’s data against this shape, SHACL will report a violation because only the stated parents are considered — absence means nonexistence.

Modeling in Agda: Type-Theoretic Foundations

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.

Core Definitions

module WorldAssumptions where

open import Data.Bool using (Bool; true; false)

open import Data.Maybe using (Maybe; just; nothing)

open import Data.Nat using (ℕ; zero; suc; _+_; _≤_)

open import Relation.Nullary using (¬_; Dec; yes; no)

open import Relation.Binary.PropositionalEquality using (_≡_; refl)-- A universe of entities

postulate Entity : Set-- Properties as relations between entities

postulate Property : Entity → Entity → Set

Open World Assumption: OWL-like Agda

In the open world, we model knowledge as what we can prove, not what we can disprove:

module OpenWorld where

open import Data.List using (List; []; _∷_; any)

open import Data.Product using (_×_; ∃; _,_; proj₁; proj₂)

record KnowledgeBase : Set₁ where

field  

  facts : List (∃ λ (subject : Entity) → ∃ λ (object : Entity) → Property subject object)


  

data OWAValue : Set where

known-true  : OWAValue  

known-false : OWAValue  

unknown     : OWAValue


  

query : KnowledgeBase → Entity → Entity → Property → OWAValue

query kb subject object prop =

if any (matches subject object prop) (KnowledgeBase.facts kb)  

then known-true  

else unknown  


  

record OntologyClass : Set₁ where

field  

  name : String  

    

    

  necessaryConditions : Entity → Set  

    

  checkSatisfiable : (e : Entity) → (kb : KnowledgeBase) →   

                    Maybe (necessaryConditions e)


  

Person : OntologyClass

Person = record

{ name = "Person"  

; necessaryConditions = λ e →   

    ∃ λ (p1 : Entity) → ∃ λ (p2 : Entity) →   

      (Property e p1 × Property e p2 × ¬ (p1 ≡ p2))  

; checkSatisfiable = λ e kb →  

      

      

    findParents e kb  

}


  

deriveNewFacts : KnowledgeBase → List Inference → KnowledgeBase

deriveNewFacts kb rules =

applyInferences kb rules


  

data QueryResult : Set where

definitely-true  : QueryResult  

definitely-false : QueryResult    

insufficient-data : QueryResult 


openWorldQuery : KnowledgeBase → Entity → Property → Entity → QueryResult  

openWorldQuery kb subj prop obj =

case lookup kb subj prop obj of  

  found-true  → definitely-true  

  found-false → definitely-false    

  not\-found   → insufficient-data 

Closed World Assumption: SHACL-like Agda

In the closed world, we can definitively determine truth values based on what’s present:

module ClosedWorld where

open import Data.List using (List; []; _∷_; length; filter)

open import Data.Nat using (ℕ; _≤?_)

open import Data.Product using (_×_; ∃; _,_)

open import Relation.Nullary using (Dec; yes; no)

record DataGraph : Set₁ where

field  

  entities : List Entity  

  triples : List (Entity × Property × Entity)  

    

  complete : Bool  


  

data CWAValue : Set where

true  : CWAValue  

false : CWAValue


  

query : DataGraph → Entity → Property → Entity → CWAValue

query dg subject prop object =

if (subject , prop , object) ∈ DataGraph.triples dg  

then true  

else false  


  

record Shape : Set₁ where

field  

  targetClass : Entity → Bool  

    

    

  constraints : List (Entity → DataGraph → Bool)


  

data ValidationResult : Set where

conforms     : ValidationResult  

violates     : List String → ValidationResult  


  

PersonShape : Shape

PersonShape = record

{ targetClass = isPersonClass  

; constraints = hasMinParents 2 ∷ \[\]  

}  

where  

  hasMinParents : ℕ → Entity → DataGraph → Bool  

  hasMinParents n entity dg =   

    let parents = countParents entity dg  

    in n ≤? parents


        countParents : Entity → DataGraph → ℕ  

  countParents entity dg =   

    length (filter (isParentTriple entity) (DataGraph.triples dg))


  

validate : DataGraph → Shape → Entity → ValidationResult

validate dg shape entity =

if all (λ constraint → constraint entity dg) (Shape.constraints shape)  

then conforms  

else violates (collectErrors dg shape entity)


  

isValid : DataGraph → Shape → Entity → Dec (ValidationResult ≡ conforms)

isValid dg shape entity =

case validate dg shape entity of  

  conforms → yes refl  

  violates \_ → no (λ ())

Bridging the Gap: Hybrid Approach

The most powerful approach combines both paradigms:

module HybridWorld where

open OpenWorld using (KnowledgeBase; OWAValue)

open ClosedWorld using (DataGraph; ValidationResult)

record HybridKnowledgeSystem : Set₁ where  

field  

    

  ontology : KnowledgeBase  

  inferenceRules : List InferenceRule


          

  instanceData : DataGraph  

  validationShapes : List Shape


          

  enrichData : DataGraph → KnowledgeBase → DataGraph


  

validateWithReasoning : HybridKnowledgeSystem → Entity → ValidationResult

validateWithReasoning hks entity =

let enrichedData \= HybridKnowledgeSystem.enrichData hks   

                    (HybridKnowledgeSystem.instanceData hks)  

                    (HybridKnowledgeSystem.ontology hks)  

in ClosedWorld.validate enrichedData shape entity  

where  

  shape \= head (HybridKnowledgeSystem.validationShapes hks)


  

inferThenValidate : KnowledgeBase → DataGraph → Shape → Entity → ValidationResult

inferThenValidate onto data shape entity =

let derived \= deriveFromOntology onto data  

  

    complete \= mergeInferred data derived  

  

in ClosedWorld.validate complete shape entity

Practical Example: Family Relationships

Let’s model a concrete example with both approaches:

module FamilyExample where

open import Data.String using (String)

\-- Entities  

postulate

alice bob charlie diana : Entity


\-- Properties  

postulate

hasParent : Property  

hasSibling : Property


\-- OWL-like ontology (OWA)  

familyOntology : OpenWorld.KnowledgeBase

familyOntology = record

{ facts \=   

    (alice , (bob , hasParent)) ∷  

    (alice , (charlie , hasParent)) ∷  

    \[\]  

}


\-- Question: Does Diana have parents?  

queryDiana : OpenWorld.OWAValue

queryDiana = OpenWorld.query familyOntology diana anyEntity hasParent

-- Result: unknown (not false!)

\-- SHACL-like validation (CWA)  

familyData : ClosedWorld.DataGraph

familyData = record

{ entities \= alice ∷ bob ∷ charlie ∷ diana ∷ \[\]  

; triples \=   

    (alice , hasParent , bob) ∷  

    (alice , hasParent , charlie) ∷  

    \[\]  

; complete \= true  

}


personShape : ClosedWorld.Shape  

personShape = record

{ targetClass \= λ \_ → true  

; constraints \= requiresExactlyTwoParents ∷ \[\]  

}


\-- Validation: Does Diana conform?  

validateDiana : ClosedWorld.ValidationResult

validateDiana = ClosedWorld.validate familyData personShape diana

-- Result: violates ["Diana has 0 parents, requires 2"]

\-- Key difference:  

-- - OWA: "We don't know if Diana has parents" (unknown)

-- - CWA: "Diana does NOT have parents" (false/violation)

Advanced: Dependent Types for Schema Evolution

One powerful application of this approach is modeling schema evolution:

module SchemaEvolution where

record EvolvingSchema (version : ℕ) : Set₁ where

field  

  classes : List OntologyClass  

    

  backwardCompatible : (v : ℕ) → v ≤ version →   

                      KnowledgeBase → Maybe ValidationResult


  

record ValidationSnapshot (version : ℕ) : Set₁ where

field  

  frozenSchema : EvolvingSchema version  

  dataAtVersion : DataGraph  

    

  mustConform : ClosedWorld.validate dataAtVersion shapes entities ≡ conforms

Type-Theoretic Insights

OWA as Intuitionistic Logic

The OWA naturally corresponds to intuitionistic/constructive logic, where:

data Proof (P : Set) : Set where

evidence : P → Proof P

-- But absence of proof is not proof of absence

-- ¬ (Proof P) does NOT imply Proof (¬ P)-- In Agda, this is natural:

openWorldNegation : {P : Set} → ¬ (Proof P) → Proof (¬ P)

openWorldNegation absence = {!!} -- Cannot be constructed!

CWA as Classical Logic with LEM

The CWA essentially adds the Law of Excluded Middle:

postulate

closed-world-LEM : (P : Set) → Dec P

-- This allows definitive validation

closedWorldNegation : {P : Set} → ¬ (Proof P) → Proof (¬ P)

closedWorldNegation {P} absence =

case closed-world-LEM P of

yes p → absurd (absence (evidence p))  

no ¬p → evidence ¬p

Modal Logic Perspective

We can also model the distinction using modal operators:

module ModalPerspective where

-- □P = "necessarily P" = proven in ontology (OWA)

-- ◇P = "possibly P" = not contradicted (OWA)

-- P = "actually P" = present in data (CWA)

record ModalKnowledge : Set₁ where  

field  

  necessary : Entity → Property → Entity → Set  -- □  

  possible  : Entity → Property → Entity → Set  -- ◇  

  actual    : Entity → Property → Entity → Bool -- P (decidable)


        -- Modal axioms  

  necessary-implies-actual : ∀ {s p o} → necessary s p o → actual s p o ≡ true  

  actual\-implies-possible  : ∀ {s p o} → actual s p o ≡ true → possible s p o

Practical Implications

When to Use OWA (OWL-like)

• Integrating data from multiple sources

• Evolving schemas over time

• Reasoning with incomplete information

• Ontology development and knowledge discovery

• Semantic web and linked data scenarios

When to Use CWA (SHACL-like)

• Data quality validation

• Database integrity constraints

• API response validation

• Form validation and user input

• Compliance checking with fixed rules

When to Use Hybrid

• Validate user input (CWA) against a rich domain model (OWA)

• Enrich incomplete data with inferred facts before validation

• Progressive validation: warn vs. error

• Multi-stage pipelines: reason (OWA) then validate (CWA)

Conclusion

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:

• Formal precision: Exact specifications of what each assumption means

• Composability: Ability to mix both approaches as needed

• Correctness: Type-checked guarantees about reasoning soundness

• Clarity: Explicit about what we know vs. what we assume

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.

To read more :

https://leanpub.com/dependenttypesdttlogicholforaiagentreadyknowledgegraphs