Skip to content

OWL / Description Logic Mapping

Status

Design todo. This explores whether the effect-contract formalism can be mapped to description logics such as OWL, or at least documented using DL notation.

Motivation

Current clauz3 contracts are relation constraints over a finite set of trusted effect facts. Many of these constraints have a natural description logic reading:

  • an operation has effect fillers
  • effect records belong to classes such as SendEmail or Withdraw
  • effect fields are data properties such as addr or amount
  • allowlists are data ranges
  • absence and maximum-cardinality contracts are class restrictions

This could give us a crisp declarative vocabulary for explaining contracts, comparing them, and possibly generating deterministic user-facing summaries.

Target Shape

For a proof target main, model one execution as an Operation individual or class whose trusted calls are linked by hasEffect.

The user example can be written in DL-like notation as:

Operation
AND (hasEffect max 1 SendEmail)
AND NOT (
  hasEffect SOME (
    SendEmail
    AND addr NOT IN {"bob@example.com", "ann@example.com"}
  )
)

Equivalently, in a more symbolic form:

Operation
  and (<= 1 hasEffect.SendEmail)
  and not exists hasEffect.(
    SendEmail
    and exists addr.(not {"bob@example.com", "ann@example.com"})
  )

This corresponds approximately to:

Email = effect("send_email")


@contract
def only(addresses: list[str]) -> ContractSpec:
    return Email.all(lambda e: e.addr in addresses)


@contract
def at_most_one_email() -> ContractSpec:
    return Email.count() <= 1

Candidate Correspondences

clauz3 concept DL / OWL-ish concept
proof target / run Operation individual or class
trusted call fact effect individual
effect("send_email") SendEmail class
fact field addr data property addr
reachable fact hasEffect filler
Email.empty() not (hasEffect some SendEmail)
Email.all(lambda e: e.addr in xs) no hasEffect filler in complement of allowed range
Email.distinct(lambda e: e.addr) key/cardinality constraint, not direct OWL DL in the general case
Email.count() <= n total effect cardinality
Email.where(lambda e: e.addr == x).count() <= n filtered effect cardinality
Withdraw.sum(lambda w: w.amount) <= n aggregate constraint, outside OWL DL

Important Semantic Mismatches

Closed World vs. Open World

clauz3 reasons over the finite effect facts generated by symbolic execution. If the prover has found all reachable trusted calls, there are no other effects.

OWL normally uses open-world semantics. Absence of a known hasEffect filler is not evidence that no such filler exists. A faithful OWL rendering would need a closure axiom or would be used only as an explanation layer, not as the primary proof semantics.

Path Conditions

Effect facts are conditional. A trusted call inside an if branch has a path condition. Relation primitives currently handle this automatically by proving constraints only for reachable facts.

A DL rendering needs a story for path conditions:

  • erase them after Z3 has discharged reachability
  • reify them as guards/provenance facts
  • or treat the DL expression as describing one concrete feasible execution

Per-Key Uniqueness

Email.distinct(lambda e: e.addr) means no two reachable SendEmail effects share the same address. This is not simply:

hasEffect max 1 SendEmail

That stronger restriction means at most one email total. Per-address uniqueness needs a key-like constraint over a data property. OWL has keys and inverse functional object properties, but data-property keyed cardinality over a finite closed trace may be better represented in Datalog, SHACL, or Z3 directly.

Aggregates

Withdraw.sum(lambda w: w.amount) <= 5 is an aggregate. OWL DL is not a natural fit for sums over related individuals. A DL view can still document the shape of the involved effects, but the numeric aggregate should remain in the relational or SMT layer.

Work Items

  1. Define a small vocabulary:
  2. Operation
  3. Effect
  4. hasEffect
  5. generated effect classes such as SendEmail, Withdraw
  6. generated data properties from trusted function parameters
  7. Write DL renderings for existing contracts:
  8. emails.none()
  9. emails.only([...])
  10. emails.unique_recipients()
  11. bank.only_account(...)
  12. bank.max_spend(...)
  13. Mark each rendering as one of:
  14. faithful OWL DL
  15. DL-shaped explanation only
  16. requires Datalog/SHACL/SMT
  17. Decide whether generated effect schemas should have optional OWL/RDF names.
  18. Explore whether DL expressions can drive deterministic natural-language summaries in the approval dialog.