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.