Back to app index

Ontologized Allen Interval Algebra — a Schedule as a Temporal CSP

This file is self-contained. Save it as ontologized-allen-schedule.html and open in any modern browser. It includes: (A) an ontology excerpt in CLIF-like first-order syntax, (B) a small Allen constraint network (the “schedule”), (C) one concrete numeric model (start/end datetimes), and (D) a checker that validates the constraints against the numeric model.

Interpretive stance: the “schedule” below is a constraint network in the signature of Allen relations. In the Grüninger–Li spirit, you can view a solution as a model of the schedule-theory plus the underlying time ontology (intervals as primitives; no timepoints).

A. Ontology excerpt (CLIF-like)

The core below is bounded meeting: primitive meets plus a derived preorder prec that guarantees upper/lower bounds, avoiding the “infinite-model pressure” of the old Infinity axiom while retaining enough structure to interpret the Allen relations. The Allen relations are then given as definitional extensions over meets.

Tbounded_meeting core axioms (reformatted) 
; ===========
; Signature:
;   TimeInterval(x)
;   meets(x,y)      ; primitive adjacency
;   prec(x,y)       ; induced ordering over intervals (preorder-ish)
; ===========

; Typing: if x meets y, both are intervals.
(forall (x y)
  (if (meets x y)
      (and (TimeInterval x) (TimeInterval y))))

; Extensional-like condition on "who meets whom" (matches the standard bounded-meeting core).
(forall (i j k m)
  (if (and (meets i k) (meets j k) (meets i m))
      (meets j m)))

; Ordering/connectedness condition: if i meets j and k meets l, either i meets l
; or there is an n that links across by a 2-step meet-chain on one side.
(forall (i j k l)
  (if (and (meets i j) (meets k l))
      (or (meets i l)
          (exists (n)
            (or (and (meets i n) (meets n l))
                (and (meets k n) (meets n j)))))))

; Asymmetry:
(forall (x y)
  (if (meets x y)
      (not (meets y x))))

; A “sum-like” axiom: three-step meet chain entails existence of a bridging meet.
(forall (i j k m)
  (if (and (meets i j) (meets j k) (meets k m))
      (exists (n) (and (meets i n) (meets n m)))))

; Boundedness: any pair has a common upper bound and a common lower bound w.r.t. prec.
(forall (x y) (exists (z) (and (prec x z) (prec y z))))
(forall (x y) (exists (z) (and (prec z x) (prec z y))))

; Definition of prec (one-step meet, or two-step meet, or equality).
(forall (x y)
  (iff (prec x y)
       (or (meets x y)
           (exists (z) (and (meets x z) (meets z y)))
           (= x y))))
Allen relations as definitional extensions over meets 
; ===========
; Allen base relations (one common axiomatisation uses these definitional patterns):
;   before, meets, overlaps, starts, during, ends, equals,
;   plus inverses after, met_by, overlapped_by, started_by, contains, ended_by
; ===========
; NOTE: "ends" here corresponds to Allen's "finishes"; "ended_by" to "finished_by".

(forall (i j)
  (iff (before i j)
       (exists (k) (and (meets i k) (meets k j)))))

(forall (i j)
  (iff (starts i j)
       (exists (k m n)
         (and (meets k i) (meets i m) (meets m n)
              (meets k j) (meets j n)))))

(forall (i j)
  (iff (ends i j)
       (exists (k m n)
         (and (meets k m) (meets m i) (meets i n)
              (meets k j) (meets j n)))))

(forall (i j)
  (iff (overlaps i j)
       (exists (k m n o p)
         (and (meets k m) (meets m n) (meets n o) (meets o p)
              (meets m j) (meets j p)
              (meets k i) (meets i o)))))

(forall (i j)
  (iff (during i j)
       (exists (k m n o)
         (and (meets k m) (meets m i) (meets i n) (meets n o)
              (meets k j) (meets j o)))))

; Inverses (definitions by converse):
(forall (i j) (iff (after i j)          (before j i)))
(forall (i j) (iff (met_by i j)        (meets j i)))
(forall (i j) (iff (started_by i j)    (starts j i)))
(forall (i j) (iff (ended_by i j)      (ends j i)))
(forall (i j) (iff (overlapped_by i j) (overlaps j i)))
(forall (i j) (iff (contains i j)      (during j i)))

; Equality-as-relation:
(forall (i j) (iff (equals i j) (= i j)))

B. The schedule as a constraint network

Think “variables = intervals” and “constraints = allowed Allen base relations between variable-pairs”. Here we mostly use singleton constraints (one base relation), but the reified constraint objects below also allow disjunctions (sets of allowed relations) if you want the full CSP(A) style.

Qualitative constraint network (human-readable)
Constraint Between Allowed Allen relation(s) Intuition
c1 Kickoff ↔ Project starts Kickoff shares the project start, ends earlier.
c2 Kickoff ↔ Design meets Design begins exactly when kickoff ends.
c3 Design ↔ Project during Design occurs strictly within the project interval.
c4 Implementation ↔ Project during Implementation occurs strictly within the project interval.
c5 Design ↔ Implementation overlaps Implementation begins before design is finished.
c6 Implementation ↔ Documentation overlaps Docs start mid-implementation and finish afterward.
c7 Implementation ↔ CodeFreeze meets CodeFreeze starts exactly when implementation ends.
c8 CodeFreeze ↔ Testing meets Testing starts exactly when code freeze ends.
c9 Testing ↔ ReleaseWindow during Testing is strictly inside the release window.
c10 ReleaseWindow ↔ Project ends Release window shares the project end, starts later.
Some consequences you can infer (composition-style)
  • meets(Kickoff, Design) ∧ overlaps(Design, Implementation) ⟹ before(Kickoff, Implementation)
  • meets(Implementation, CodeFreeze) ∧ meets(CodeFreeze, Testing) ⟹ before(Implementation, Testing)
  • during(Testing, ReleaseWindow) ∧ ends(ReleaseWindow, Project) ⟹ during(Testing, Project)

In CSP terms: these are entailments in the Allen theory (or its synonymous bounded-meeting ontology), i.e. constraints you can propagate.

C. One concrete model (grounding with datetimes)

The datetimes below are just a satisfying interpretation. Your “schedule” remains meaningful even before you pick dates, but once you pick them you can validate constraints (and potentially learn your qualitative network was inconsistent).

Primary schedule intervals
Interval Start (UTC) End (UTC)
Witness intervals (optional) — temporal parts that make “overlaps” reducible to meets

In the meets-based definitional extension, relations like overlaps(i,j) are witnessed by additional intervals (often interpretable as temporal parts/gaps). Below we explicitly name a few such witnesses for overlaps(Design, Implementation).

Witness interval Start (UTC) End (UTC) Role
Witnessed meets-facts (one concrete Skolemization) 

      

    

  


  
D. Data in JSON-LD (ontology-friendly “in HTML” encoding)

  

    This JSON-LD reifies each Allen constraint as an object (AllenConstraint) whose allowed field is a set of admissible relations;
    that’s the natural encoding for a temporal CSP network where constraints can be disjunctions.
  


  

    Show JSON-LD payload
    

  


  
E. Constraint checker (computed Allen base relations)

  

    The table below is computed by comparing starts/ends of each pair and classifying them into one of Allen’s 13 base relations.
    It then checks whether the computed relation is in the constraint’s allowed set.
  


  

    Results
    

      
        

          Constraint
          X
          Allowed
          Y
          Computed
          Status
        

      
      
        
      
    


    
Derived checks (not asserted as constraints)

    

      
        

          Derived statement
          Computed relation
          Holds?
        

      
      
    

  


  

  

  


  

    If you want to push this toward a “real” solver: replace the concrete start/end fields with domains
    (or leave them blank), allow disjunctive constraint sets, and run path-consistency / algebraic closure against the Allen composition table;
    the ontological move is that satisfiable networks correspond to models of the underlying time ontology rather than mere spreadsheet coherence.