The Algorithm: How DDIC Resolves Conflicts

Two rules contradict each other: a nurse is not allowed to read patient records, but in an emergency, she is. Which one wins? How does the engine prove this in microseconds, without a theorem prover and without magic?

FC
Frank Csehan
· 12 min read

The last post was about how rules get into the guard: forms instead of free text, the LLM fills in fields, a deterministic function generates the MELD syntax. I promised at the end that this time it would be about the engine itself. By that I mean the point where two rules contradict each other, both correctly formulated, both active, and the engine still has to deliver an answer in microseconds.

When you hear “deontic logic”, you quickly think of university seminars, modal operators and proofs at the blackboard. Then of runtime, of milliseconds that add up to seconds when a hundred agents want something at the same time. But it’s not that bad. The algorithm is a sorted list traversal with a few pairwise comparisons. There is neither a theorem prover nor a SAT solver like Z3 behind it.

The scenario

Back to our hospital example. The compliance officer has laid down three rules:

  1. Nursing staff are not permitted to view patient records.
  2. During night shifts, when no doctor is available, nursing staff are permitted to view patient records.
  3. Medical data is never disclosed to external parties.

The third rule is a moral axiom and stands above everything else. The first two are context-dependent and conflict with one another. In MELD, this looks like this:

; Rule 1: General house rule
(forbiddenToDo-WRT HospitalCode nursing
    (readPatientRecord patientRecord))

; Rule 2: Exception for the night shift
(permittedToDo-WRT EmergencyCode nursing-nightshift
    (readPatientRecord patientRecord))

; Rule 3: Moral axiom
(forbiddenToDo nursing
    (forwardData medical external))

A nurse on night duty calls: she wants to view the patient record. The Guard receives the request and now has to decide: PERMITTED, FORBIDDEN or UNDECIDABLE. The algorithm runs in this order.

Step 1: Who does the rule actually concern?

Before I talk about conflicts, the engine filters the rules that are actually applicable. A rule is applicable if it concerns the agent and describes the requested action. So the engine asks: Which rules address this specific request?

applicable = [
    n for n in norms
    if n.matches_agent(agent)
    and self._proposition_matches(n, proposition)
]

matches_agent uses the ontology. If the rule applies to nursing and the agent is nursing-nightshift, and the ontology states (genls nursing-nightshift nursing), then the rule matches. nursing-nightshift is a specialisation of nursing. Inheritance works downwards.

For our scenario, two rules remain after the filter: Rule 1 and Rule 2. Rule 3 refers to a different action (forwardData) and is not applicable.

Under the hood, proposition_matches works with unification. That is why a rule with the pattern ("readPatientRecord",) also matches a request with additional parameters, which a string comparison would not. This is a Prolog technique from the seventies, applied in a new way. The filter itself is O(n). With ten thousand rules per domain, this still amounts to microseconds, because each rule is handled with a dictionary lookup and a tuple comparison.

Step 2: Axioms always win

Before anything else, the engine separates out the moral axioms. In the NormFrame data structure, there is a flag defeasible: bool. True means overridable, False means axiom.

axioms = [n for n in applicable if not n.defeasible]
defeasible = [n for n in applicable if n.defeasible]

if axioms:
    # Are there conflicting axioms? Then UNDECIDABLE.
    if detect_conflicts(axioms):
        return NormStatus(modality=None, reason="contradictory_axioms", ...)
    # Otherwise: the axiom wins, full stop.
    return NormStatus(modality=axioms[0].modality, reason="moral_axiom", ...)

An applicable axiom decides, without context dependency. If two axioms contradict each other, the engine returns UNDECIDABLE, and the surrounding infrastructure blocks the action. Fail-closed. I’d rather live with a false positive than with an action that should never have happened. In our scenario, there is no axiom in the filter set. Rule 3 deals with passing on data and says nothing about reading it. The engine continues.

Step 3: Specificity as an organising principle

Rule 1 and Rule 2 contradict each other. Rule 1 prohibits, Rule 2 permits. Both can be overridden, both are active, and I must decide which one wins.

DDIC replies: the more specific one. Specificity here is an integer. Each rule has a field specificity: int, which is calculated from the depth in the inheritance hierarchy when the MELD file is read in. nursing has depth 2, nursing-nightshift has depth 3. The rule for nursing-nightshift is more specific.

# Sort defeasible norms by specificity, descending
applicable_sorted = sorted(
    defeasible,
    key=lambda n: (n.specificity, code_rank, n.code, n.modality.value),
    reverse=True,
)

# Preemption: a more specific rule defeats a more general one
for i, a in enumerate(sorted_norms):
    for j, b in enumerate(sorted_norms):
        if j <= i or not a.conflicts_with(b):
            continue
        if a.specificity > b.specificity:
            defeated.add(j)
        elif b.specificity > a.specificity:
            defeated.add(i)
            break

A double-loop comparison. O(n²) in the worst-case scenario, rarely relevant in practice because n (the number of applicable rules after filtering) is almost never more than a dozen. For every applicable rule against every other: is there a conflict, and if so, which is more specific? The less specific one is discarded.

Rule 2 (specificity=3) beats Rule 1 (specificity=2). The engine responds PERMITTED.

Incidentally, the sort key is a tuple: (specificity, code_rank, code, modality_value). The latter fields act as tiebreakers and guarantee determinism even in the event of a tie. The conflict check conflicts_with, in turn, is a set comparison of the modalities. PERMITTED and FORBIDDEN conflict, OBLIGATORY and PERMITTED do not, because obligation implies permission. The core of Olson’s calculus fits into three lines of Python at this point.

Step 4: When specificity is not enough

What do I do if two rules are equally specific? For example, one comes from the HospitalCode and the other from the GDPRCode. Both apply to doctor, both concern readPatientRecord, one permits it and the other prohibits it. Same depth in the hierarchy, no pre-emption.

At this point code precedence applies. At startup, the engine receives a list code_prevalence: ["GDPRCode", "HospitalCode"]. Earlier entries win against later ones. Legal rules rank above house rules.

def _resolve_by_prevalence(self, norms):
    by_modality = group_by_modality(norms)
    best_modality, best_rank = None, -1
    for modality, mod_norms in by_modality.items():
        for n in mod_norms:
            rank = prevalence_rank(n.code)
            if rank > best_rank:
                best_rank, best_modality = rank, modality
    # Check if the rank is unique
    if tie_exists(best_rank, by_modality):
        return None  # UNDECIDABLE
    return by_modality[best_modality]

If the precedence is clear, the higher-ranking code wins. If two rules come from the same code and are still contradictory, or if two codes are of equal rank, what remains is UNDECIDABLE.

Step 5: UNDECIDABLE

return NormStatus(
    modality=None,
    reason="unresolved_conflict",
    justification_chain=tuple(chain),
)

modality=None. The engine says neither “I suspect FORBIDDEN” nor “I’ll take the first rule”. It says: I cannot decide. The surrounding infrastructure interprets this state as fail-closed. The action does not go ahead. A human takes a look.

I believe this is the part that many people who build rule sets underestimate. Most systems have an implicit default: allow when unclear, or prohibit when unclear. Both are wrong in critical contexts. The first approach opens up loopholes that nobody has documented. The second produces false alarms that nobody takes seriously anymore. UNDECIDABLE is a third state that says explicitly: the rule set is incomplete here. The problem then lies in the specification.

How do you know all this is correct?

An algorithm that decides on the behaviour of AI systems must be demonstrably correct. “Looks right” is not enough. I underestimated how much work this proof involves. The work lies less in the engine itself than in everything around it, the part that shows: it does what it is supposed to do.

AEGIS has a four-stage verification chain for this. Each stage catches a different class of errors. From concrete examples in the research literature to a machine-verified model.

Stage 1: The examples from Olson’s dissertation

The entire algorithm is derived from Taylor Olson’s work at Northwestern University. His dissertation, “A Formal Theory of Norms”, from June 2025, is the reference. It contains four concrete example scenarios with which Olson explains his calculus. A patient named Karli who tells a care robot which information it is permitted to pass on to whom.

These four scenarios are represented as Python tests. If any of them fails, the implementation has not understood Olson’s calculus at this point.

Stage 2: Olson’s complete conflict matrix

Olson lists the expected outcome for every conceivable combination of norm type and subsumption relation. It is his own summary of what his calculus must do.

Stage 3: Exhaustive combinatorics

Olson’s table covers the conflict cases he describes theoretically. But a real engine gets not only the cases the author had in mind, but everything that humans or LLMs write into a rule set.

So the third test stage is tied to the engine’s own parameter space, independent of Olson’s theorems. The algorithm has four input dimensions that determine the result:

Six times three times four times three gives two hundred and sixteen combinations. The expected result is derived programmatically from Olson’s rules.

Two hundred and sixteen is the complete enumeration of the relevant parameter space. If a cell fails here, I not only know that something is wrong, but exactly which constellation is causing the problem.

Stage 4: The TLA+ model

Tests check specific inputs. They do not check that there is no input that causes a problem. For that you need a formal model.

TLA+ is a formal specification language by Leslie Lamport, designed to describe concurrency and state machines in a machine-checkable way. The model describes the six-step algorithm as a state machine. Each step is a transition between states. On top of that, invariants are formulated, statements that must be true in every reachable state. For example:

The TLC Model Checker is the tool that executes a TLA+ specification and searches the state space. It tries out all reachable states. For each state, it checks whether the invariants hold. If it finds a counterexample path, it displays it. For up to four simultaneously active norms with three modalities, four specificity levels and two codes, this is a finite but large set. TLC checks it completely.

Supplementary property tests

Then there are tests that target individual properties of the engine. No new scenarios, but they harden the algorithm against regressions. The most important is axiom monotonicity, the guarantee that an axiom is never defeated by an overridable rule. Hypothesis is a Python library for property-based testing. Instead of fixed examples it generates random inputs automatically and searches for counterexamples. With it, four hundred random scenarios are generated, each containing between one and fifty overridable rules plus one axiom. The invariant: the axiom wins. No counterexample in any run.

The rest is bookkeeping, but important: Determinism (same input, same output, even across parallel threads and randomly shuffled norms), Totality (the algorithm terminates, always), the duality forbidden(X) ↔ ¬permitted(X), the Closed World Assumption for registered actions without a permission rule. Each of these properties has its own test suite, and every one of them passes. It is painstaking work, and it is what later gives you the confidence to commit a change to the algorithm without lying awake at night.

What the verification chain achieves

The individual stages can be seen as filters, each catching a different class of errors. Stage one catches misunderstandings of the theory: if Olson’s examples cannot be reproduced, his calculus has simply not been understood. Gaps between the examples are caught by stage two, because Olson’s table covers cases that he does not explicitly go through in the individual examples. The combinatorics in stage three then catches the gaps between the table rows, the non-conflicting pairs and defeasibility combinations about which Olson says nothing theoretically. In stage four, the TLA+ model catches the errors that no specific input triggers, the invariants that must hold in all states. The supplementary tests act as a safety net against regressions in individual properties.

Together, this amounts to over three hundred and sixty formal tests, plus the TLA+ model and the equivalence tests between the two evaluators. None of this replaces a universal proof. But each stage rules out classes of errors, and that is more verification than most production systems have.

Confidence in the algorithm rests on the fact that it reproduces Olson’s published examples, satisfies his table row by row, runs through the entire parameter space exhaustively and holds against the formal invariants under TLC. This verification chain is documented and can be reproduced at any time.

What this means in microseconds

In our scenario, the engine runs in under ten microseconds because the algorithm does so little: filtering a list, a bit of sorting, a few pairwise comparisons. The speed of Python has nothing to do with it.

That means you can run every single action of an AI agent through this guard without the agent becoming noticeably slower. The bottleneck is the agent itself, because an LLM round trip takes several orders of magnitude longer than the DDIC evaluation.

AI AEGIS MELD DDIC Architecture