Lex: A Formal Ontology Language for Property Graphs

Property graphs have become the dominant paradigm for modeling connected data, yet they lack the formal semantic rigor that RDF/OWL brought to knowledge representation. While RDF graphs are constrained by their triple-based structure, property graphs offer richer modeling capabilities through typed edges with properties. However, this expressiveness comes at a cost: the absence of standardized formal semantics and constraint languages that can reason about graph structure and properties simultaneously.

Enter Lex (Logical Expression language for graphs) — a formal ontology language specifically designed for property graphs that brings the rigor of description logic to the flexibility of the property graph model.

The Property Graph Gap

Property graphs, popularized by systems like Neo4j, TigerGraph, and Amazon Neptune, represent knowledge as nodes and edges where both can carry arbitrary key-value properties. This model naturally captures real-world entities and relationships:

(:Person {name: "Alice", age: 30})-[:KNOWS {since: 2015}]->(:Person {name: "Bob"})

However, property graphs traditionally lack:

Formal semantics for reasoning about graph structure

Type constraints beyond simple labels

Axioms that express logical relationships between patterns

Inference rules that derive new knowledge from existing patterns

RDF/OWL provided these capabilities but forced everything into subject-predicate-object triples, making it awkward to represent multi-property relationships. Lex bridges this gap.

Core Concepts in Lex

Node Types and Edge Types

Lex treats node labels and edge types as first-class ontological concepts:

NodeType Person { properties: { name: String [required], age: Integer [min: 0, max: 150], email: String [unique] }}

EdgeType KNOWS { source: Person, target: Person, properties: { since: Date [required], strength: Float [min: 0.0, max: 1.0] }}

This declaration establishes both structural constraints (what properties must exist) and value constraints (what ranges are valid).

Property Constraints

Lex supports rich property-level constraints beyond simple type checking:

NodeType Employee extends Person {
properties: {
employeeId: String [unique, pattern: /^EMP\d{6}$/],
salary: Float [min: 0],
department: String [enum: ["Engineering", "Sales", "HR"]],
manager: Reference<Employee> [optional] },
constraints: {
// Self-reference constraint assert manager != self,
// Cross-property constraint assert age >= 18,
// Cardinality constraint assert count(outgoing(MANAGES)) <= 10
}}

These constraints are validated at write time and can trigger inference at read time.

Axioms: Deriving Knowledge from Structure

Axioms in Lex define logical relationships between graph patterns. They enable reasoning about implicit knowledge based on explicit structure.

Transitivity Axioms

Axiom TransitiveAncestor {
pattern: (a:Person)-[:PARENT_OF]->(b:Person)-[:PARENT_OF]->(c:Person),
infers: (a)-[:ANCESTOR_OF]->(c)
}

This axiom states: if A is parent of B, and B is parent of C, then A is an ancestor of C. The inference engine can materialize these ANCESTOR_OF edges or compute them on-demand.

Symmetry Axioms

Axiom SymmetricFriendship {
pattern: (a:Person)-[k:KNOWS {mutual: true}]->(b:Person),
infers: (b)-[:KNOWS {mutual: true}]->(a)
}

When a mutual friendship exists in one direction, Lex ensures it exists in both.

Property Propagation Axioms

Axiom InheritCompanyRisk {
pattern: (e:Employee)-[:WORKS_FOR]->(c:Company {riskLevel: ?risk}),
infers: e.exposureRisk = ?risk}

This propagates company risk levels to employees, demonstrating how axioms can derive node properties from graph context.

Existential Axioms

Axiom ManagerMustBeEmployee {
pattern: (e:Employee {manager: ?m}),
requires: exists (m:Employee)}

This ensures referential integrity: every manager reference must point to an actual Employee node.

Complex Constraints Through Path Patterns

Lex supports path-based constraints that reason about graph structure:

NodeType Department {
properties: { name: String [required], budget: Float }, constraints: { // No circular reporting structures assert not exists path (self)-[:REPORTS_TO*1..]->(self), // Must have at least one employee assert count(incoming(WORKS_IN)) >= 1, // Budget must cover salaries assert this.budget >= sum(incoming(WORKS_IN).source.salary) }}

The path construct allows expressing topological constraints that prevent cycles, ensure connectivity, or validate hierarchical structures.

Temporal Axioms and Versioning

Lex recognizes that knowledge graphs evolve over time:

EdgeType EMPLOYED_BY { source: Person, target: Company, properties: { startDate: Date [required], endDate: Date [optional], role: String }}

Axiom CurrentEmployment { pattern: (p:Person)-[e:EMPLOYED_BY {endDate: null}]->(c:Company), infers: (p)-[:CURRENTLY_WORKS_FOR]->(c)}Constraint NoOverlappingEmployment { pattern: (p:Person)-[e1:EMPLOYED_BY]->(c1), (p)-[e2:EMPLOYED_BY]->(c2), requires: (e1.endDate < e2.startDate) OR (e2.endDate < e1.startDate) OR (e1 == e2)}

These temporal patterns ensure employment periods don’t overlap and derive current employment status.

Probabilistic Axioms

Unlike classical description logics, Lex can express probabilistic inference:

ProbabilisticAxiom LikelyInterest { pattern: (p1:Person)-[:FOLLOWS]->(p2:Person)-[:INTERESTED_IN]->(t:Topic), infers: (p1)-[:MIGHT_LIKE {confidence: 0.6}]->(t), // Strength increases with shared connections boost: count((p1)-[:FOLLOWS]->(:Person)-[:INTERESTED_IN]->(t)) * 0.1}

This creates weighted recommendations based on social graph patterns, where confidence scores accumulate through multiple paths.

Negation and Open World Assumptions

Lex supports both closed world (absence means false) and open world (absence means unknown) reasoning:

Axiom NoKnownAllergies { pattern: (p:Person), requires: not exists (p)-[:ALLERGIC_TO]->(:Substance), infers: p.clearForAllIngredients = true, // Only valid under closed world assumption worldAssumption: closed(ALLERGIC_TO)}

The worldAssumption annotation makes explicit when an axiom depends on complete information.

Integration with Dependent Types

Given your interest in dependent type theory, Lex can be extended with dependent types on graph patterns:

DependentNodeType Vector(dim: Nat) { properties: { components: Array<Float>[length: dim] }}

DependentEdType SIMILARITY(v1: Vector(?d1), v2: Vector(?d2)) where d1 == d2 { properties: { score: Float [min: -1.0, max: 1.0] }, constraints: { // Enforce computed similarity assert score == dotProduct(v1.components, v2.components) / (norm(v1.components) * norm(v2.components)) }}

This ensures vectors can only be compared if they have matching dimensions, bringing type-level guarantees to graph operations.

Practical Implementation Considerations

Lex ontologies compile to different enforcement strategies:

Eager validation: Constraints checked on write operations

Materialized inference: Axioms computed and stored as new edges/properties

Virtual inference: Axioms computed on-demand during queries

Hybrid approaches: Critical inferences materialized, others virtual

The choice depends on graph size, update frequency, and query patterns:

Axiom TransitiveAncestor { pattern: (a:Person)-[:PARENT_OF]->(b:Person)-[:PARENT_OF]->(c:Person), infers: (a)-[:ANCESTOR_OF]->(c), // Implementation hint strategy: materialized, updateTrigger: onChange(PARENT_OF)}

Comparison with Existing Approaches

Press enter or click to view image in full size

Conclusion

Lex brings formal semantics to property graphs without sacrificing their expressive power. By supporting rich constraints, logical axioms, temporal patterns, and even dependent types, it provides a foundation for reasoning about connected data that goes beyond simple validation.

For systems requiring both the flexibility of property graphs and the rigor of formal ontologies — whether in knowledge management, regulatory compliance, or agentic AI systems — Lex offers a path forward that doesn’t force choosing between expressiveness and correctness.

The language remains a research direction worth exploring as property graphs continue to dominate practical knowledge representation, yet increasingly demand the semantic guarantees that only formal ontologies can provide.