Open World vs Closed World: Modeling OWL and SHACL Semantics in Agda

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.