Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Capability Safety as Datalog: A Foundational Equivalence

Cosimo Spera

Abstract

We prove that capability safety admits an exact representation as propositional Datalog evaluation (Datalogprop: the monadic, ground, function-free fragment of first-order logic), enabling the transfer of algorithmic and structural results unavailable in the native formulation. This addresses two structural limitations of the capability hypergraph framework of Spera [2026]: the absence of efficient incremental maintenance, and the absence of a decision procedure for audit surface containment. The equivalence is tight: capability hypergraphs correspond to exactly this fragment, no more.

Capability Safety as Datalog: A Foundational Equivalence

Abstract

We prove that capability safety admits an exact representation as propositional Datalog evaluation (Datalogprop: the monadic, ground, function-free fragment of first-order logic), enabling the transfer of algorithmic and structural results unavailable in the native formulation. This addresses two structural limitations of the capability hypergraph framework of Spera [2026]: the absence of efficient incremental maintenance, and the absence of a decision procedure for audit surface containment. The equivalence is tight: capability hypergraphs correspond to exactly this fragment, no more.

Paper Structure

This paper contains 43 sections, 11 theorems, 22 equations.

Table of Contents

  1. Introduction
  2. A New Computational Lens for Agentic Safety
  3. What is Datalog?
  4. The Propositional Fragment
  5. Contributions
  6. Related Work
  7. Datalog and descriptive complexity.
  8. Datalog provenance and semirings.
  9. Logic-based learning and Horn clause learning.
  10. AI safety formalisms.
  11. View update and incremental maintenance.
  12. Formal Background
  13. Capability Hypergraphs
  14. Propositional Datalog
  15. Provenance Semirings
  16. ...and 28 more sections

Key Result

Theorem 4.3

Let $H=(V,\mathcal{F})$ be a capability hypergraph and $A\subseteq V$. Under Definition def:encoding-cap-dl:

Theorems & Definitions (38)

  • Definition 3.1: Capability Hypergraph
  • Definition 3.2: Closure Operator
  • Definition 3.3: Safe Region and Minimal Unsafe Antichain
  • Definition 3.4: Emergent Capabilities and Near-Miss Frontier
  • Definition 3.5: Safe Audit Surface
  • Definition 3.6: Propositional Datalog Program
  • Definition 3.7: Datalog Query and Minimal Witness
  • Definition 4.1: The $\text{CapHyp}\to\text{Datalog}_{\mathsf{prop}}$ Encoding
  • Remark 4.2: Stratified Negation
  • Theorem 4.3: Encoding Correctness: $\text{CapHyp}\to\text{Datalog}_{\mathsf{prop}}$
  • ...and 28 more