A Normative Intermediate Representation for ASP-Based Compliance Reasoning

# A Normative Intermediate Representation for ASP-Based Compliance Reasoning
Source: [https://arxiv.org/html/2606.04619](https://arxiv.org/html/2606.04619)
###### Abstract

We propose MONIR, a Modalized\-Output Normative Intermediate Representation for ASP\-based compliance reasoning\. Its core fragment has a staged operational semantics, while MONIR\-ASP provides an executable compilation and extensions for external functions, temporal rules, and stable\-model reasoning\. We instantiate the framework on Chinese ADAS regulations and standards with an LLM\-assisted pipeline\. Experiments evaluate extraction quality and the efficiency of modular and incremental ASP solving\.

## Introduction

Compliance checking for technical standards requires executable and explainable representations of normative clauses\. This is challenging because standards combine factual conditions with modalities, exceptions, compensations, conflicts, and uncertainty\. Although LLMs can extract structured rules from text, symbolic reasoning still requires a stable intermediate representation\.

Answer Set Programming \(ASP\)\(Brewkaet al\.[2011](https://arxiv.org/html/2606.04619#bib.bib8)\)is a suitable backend for this task\. Recent work also reports strong solver performance for compliance checking tasks\(Robaldoet al\.[2024](https://arxiv.org/html/2606.04619#bib.bib9)\)\. However, directly encoding standards in ASP often hides the roles of conditions, modalities, targets, exemptions, and violations inside implementation predicates\. This makes LLM\-generated rule bases harder to inspect, repair, and explain\.

This paper proposes MONIR, short for Modalized\-Output Normative Intermediate Representation\. MONIR is inspired in part by the input\-output view of conditional norms\(Makinson and van der Torre[2000](https://arxiv.org/html/2606.04619#bib.bib1)\), but it is not intended as a full deontic logic\. It is a restricted intermediate language for connecting LLM\-assisted norm extraction with ASP\-based compliance reasoning\. A MONIR rule separates the condition under which a norm applies from the modalized target it produces, and treats exemption as a rule\-level output rather than as a deontic modality\.

![Refer to caption](https://arxiv.org/html/2606.04619v1/x1.png)Figure 1:Overall workflow of the proposed framework\. Natural\-language standards are transformed into MONIR rule bases, while configuration forms are compiled into ASP facts\. MONIR\-ASP executes the resulting reasoning task with modular and incremental solving, and produces violations, conflicts, unknown states, explanations, and compliance status\.Figure[1](https://arxiv.org/html/2606.04619#Sx1.F1)shows the workflow\. The norm extraction lane maps standard clauses into MONIR rules\. The fact preparation lane maps configuration forms into ASP facts\. The resulting objects are compiled into MONIR\-ASP, where proposition modules and norm modules can be evaluated and updated separately under the ASP module theorem\(Oikarinen and Janhunen[2006](https://arxiv.org/html/2606.04619#bib.bib11)\)\. When user\-confirmed updates arrive, the system reuses unaffected module results and re\-solves affected parts through multi\-shot ASP solving\(Gebseret al\.[2019](https://arxiv.org/html/2606.04619#bib.bib10)\)\.

The paper makes three contributions\. First, it defines MONIR\-core, including its syntax, admissibility conditions, staged operational semantics, and basic meta\-theoretic properties\. Second, it gives MONIR\-ASP, an executable ASP realization of MONIR with extensions for external proposition functions, temporal encodings, and stable\-model semantics beyond the core fragment\. Third, it implements an LLM\-assisted ADAS compliance\-checking pipeline and evaluates both extraction quality and solving efficiency\.

## Preliminaries

This section reviews the background used in the paper: ASP for rule\-based reasoning and LLM\-assisted extraction for mapping regulatory text to structured rules\.

### Answer Set Programming

Answer Set Programming \(ASP\) is a declarative framework\. A term is a constant, a variable, or a function term\. A term is ground if it contains no variables\. Ifppis annn\-ary predicate symbol andt1,…,tnt\_\{1\},\\ldots,t\_\{n\}are terms, thenp​\(t1,…,tn\)p\(t\_\{1\},\\ldots,t\_\{n\}\)is an atom\. For a ground programΠ\\Pi, let𝖠𝗍​\(Π\)\\mathsf\{At\}\(\\Pi\)be the set of ground atoms occurring inΠ\\Pi\. An interpretation is a setX⊆𝖠𝗍​\(Π\)X\\subseteq\\mathsf\{At\}\(\\Pi\)\. A normal rulerrhas the form

a0←a1,…,am,𝗇𝗈𝗍​am\+1,…,𝗇𝗈𝗍​an\.\\displaystyle a\_\{0\}\\leftarrow a\_\{1\},\\ldots,a\_\{m\},\\mathsf\{not\}\\ a\_\{m\+1\},\\ldots,\\mathsf\{not\}\\ a\_\{n\}\.where𝗇𝗈𝗍\\mathsf\{not\}denotes negation as failure\. We writeH​\(r\)=\{a0\}H\(r\)=\\\{a\_\{0\}\\\},B\+​\(r\)=\{a1,…,am\}B^\{\+\}\(r\)=\\\{a\_\{1\},\\ldots,a\_\{m\}\\\},B−​\(r\)=\{am\+1,…,an\}B^\{\-\}\(r\)=\\\{a\_\{m\+1\},\\ldots,a\_\{n\}\\\}\. An integrity constraint is a rule with empty head, written as←B\.\\leftarrow B\.It eliminates interpretations satisfyingBB\.

For a ground normal program, stable model semantics is defined by the Gelfond–Lifschitz reduct\(Gelfond and Lifschitz[1988](https://arxiv.org/html/2606.04619#bib.bib7)\)\. Given an interpretationXX, the reduct ofΠ\\Piwith respect toXXis the program

ΠX=\{H​\(r\)←B\+​\(r\)∣r∈Π,B−​\(r\)∩X=∅\}\.\\Pi^\{X\}=\\\{H\(r\)\\leftarrow B^\{\+\}\(r\)\\mid r\\in\\Pi,\\ B^\{\-\}\(r\)\\cap X=\\emptyset\\\}\.The set of stable models ofΠ\\Pi, denoted by𝖲𝖬​\(Π\)\\mathsf\{SM\}\(\\Pi\), is defined by

X∈𝖲𝖬​\(Π\)​iff​X​is a⊆\-minimal model of​ΠX\.X\\in\\mathsf\{SM\}\(\\Pi\)\\ \\text\{iff\}\\ X\\text\{ is a \}\\subseteq\\text\{\-minimal model of \}\\Pi^\{X\}\.The set of stable models is denoted by𝖲𝖬​\(Π\)\\mathsf\{SM\}\(\\Pi\)\. For a non\-ground programΠ\\Piand input factsFF, grounding produces𝗀𝗋​\(Π,F\)\\mathsf\{gr\}\(\\Pi,F\), and solving computes𝖲𝖬​\(𝗀𝗋​\(Π,F\)\)\\mathsf\{SM\}\(\\mathsf\{gr\}\(\\Pi,F\)\)\.

To support staged and modular computation, we use ASP modules\(Oikarinen and Janhunen[2006](https://arxiv.org/html/2606.04619#bib.bib11)\)\. A module is a tuple𝒫=⟨R,I,O,H⟩\\mathcal\{P\}=\\langle R,I,O,H\\rangle, whereRRis the rule set andII,OO, andHHare pairwise disjoint input, output, and hidden signatures\. Head atoms inRRbelong toO∪HO\\cup H\. ForV⊆IV\\subseteq I, letR\[V\]=R∪\{a←∣a∈V\}R\[V\]=R\\cup\\\{a\\leftarrow\\mid a\\in V\\\}\. The stable models of𝒫\\mathcal\{P\}underVVare

𝖲𝖬​\(𝒫,V\)=\{X∈𝖲𝖬​\(R​\[V\]\)∣X∩I=V\}\.\\mathsf\{SM\}\(\\mathcal\{P\},V\)=\\\{X\\in\\mathsf\{SM\}\(R\[V\]\)\\mid X\\cap I=V\\\}\.
Two modules𝒫1=⟨R1,I1,O1,H1⟩\\mathcal\{P\}\_\{1\}=\\langle R\_\{1\},I\_\{1\},O\_\{1\},H\_\{1\}\\rangleand𝒫2=⟨R2,I2,O2,H2⟩\\mathcal\{P\}\_\{2\}=\\langle R\_\{2\},I\_\{2\},O\_\{2\},H\_\{2\}\\rangleare joinable if:

1. 1\.O1∩O2=∅O\_\{1\}\\cap O\_\{2\}=\\emptyset;
2. 2\.H1∩𝖠𝗍​\(𝒫2\)=∅H\_\{1\}\\cap\\mathsf\{At\}\(\\mathcal\{P\}\_\{2\}\)=\\emptysetandH2∩𝖠𝗍​\(𝒫1\)=∅H\_\{2\}\\cap\\mathsf\{At\}\(\\mathcal\{P\}\_\{1\}\)=\\emptyset;
3. 3\.no strongly connected component in the positive dependency graph contains output atoms from bothO1O\_\{1\}andO2O\_\{2\}\.

Here, the positive dependency graph uses edges from heads to positive body atoms; condition 3 forbids cross\-module positive recursion but permits negative dependencies\.

Let𝒫1⊔𝒫2\\mathcal\{P\}\_\{1\}\\sqcup\\mathcal\{P\}\_\{2\}denote the composition of two joinable modules\. Two local resultsX1X\_\{1\}andX2X\_\{2\}are compatible, writtenX1∼X2X\_\{1\}\\sim X\_\{2\}, iff they agree on their shared visible atoms:

X1∩𝖠𝗍​\(𝒫2\)=X2∩𝖠𝗍​\(𝒫1\)\.X\_\{1\}\\cap\\mathsf\{At\}\(\\mathcal\{P\}\_\{2\}\)=X\_\{2\}\\cap\\mathsf\{At\}\(\\mathcal\{P\}\_\{1\}\)\.The module theorem justifies evaluating joinable modules separately and merging compatible stable models\.

### LLM\-Assisted Extraction

Large language models \(LLMs\) are typically formulated as autoregressive generative models\. Given a contextCC, an LLM parameterized byθ\\thetagenerates an output sequencey=\(y1,…,yT\)y=\(y\_\{1\},\\ldots,y\_\{T\}\)according to

pθ​\(y∣C\)=∏t=1Tpθ​\(yt∣C,y<t\)\.p\_\{\\theta\}\(y\\mid C\)=\\prod\_\{t=1\}^\{T\}p\_\{\\theta\}\(y\_\{t\}\\mid C,y\_\{<t\}\)\.This formulation enables LLMs to perform various tasks through natural\-language instructions and few\-shot demonstrations, without task\-specific parameter updates\(Brownet al\.[2020](https://arxiv.org/html/2606.04619#bib.bib16)\)\.

We consider structured extraction as a special case of prompt\-conditioned generation\. Let𝒳\\mathcal\{X\}denote the space of natural\-language inputs and𝒴\\mathcal\{Y\}a structured output language\. An ideal extractor is represented by an oracleΩ:𝒳→𝒴\\Omega:\\mathcal\{X\}\\rightarrow\\mathcal\{Y\}, which maps an inputxxto the desired structurey∗=Ω​\(x\)y^\{\\ast\}=\\Omega\(x\)\. An LLM\-assisted extractor takes a promptCCand an inputxx, and producesy^=decθ⁡\(C,x\)∈𝒴\\hat\{y\}=\\operatorname\{dec\}\_\{\\theta\}\(C,x\)\\in\\mathcal\{Y\}, wheredecθ\\operatorname\{dec\}\_\{\\theta\}denotes the decoding procedure induced by the LLM\.

Thus, structured extraction can be viewed as constrained generation over𝒴\\mathcal\{Y\}, aiming to makey^\\hat\{y\}close to the oracle outputΩ​\(x\)\\Omega\(x\)under a task\-specific discrepancy measure\.

## MONIR\-core: Syntax and Operational Semantics

This section defines MONIR\-core, the core fragment of MONIR, including its syntax, admissibility conditions, operational semantics, and basic properties\.

### Syntax

MONIR\-core is defined over a finite vocabulary𝒱=⟨𝒫,𝒩,ℳ,𝒮⟩\\mathcal\{V\}=\\langle\\mathcal\{P\},\\mathcal\{N\},\\mathcal\{M\},\\mathcal\{S\}\\rangle, where𝒫\\mathcal\{P\}contains atomic propositions,𝒩\\mathcal\{N\}rule identifiers,ℳ\\mathcal\{M\}normative modalities, and𝒮\\mathcal\{S\}rule\-state symbols\. In MONIR\-core,

ℳ=\{𝖮,𝖥,𝖯,𝖱,𝖭𝖱\},\\mathcal\{M\}=\\\{\\mathsf\{O\},\\mathsf\{F\},\\mathsf\{P\},\\mathsf\{R\},\\mathsf\{NR\}\\\},standing for obligation, prohibition, permission, recommendation, and negative recommendation\. Exemption is represented as a rule\-level output\. The rule\-state symbols are

⟨𝗉𝖾𝗇𝖽𝗂𝗇𝗀,𝗈𝗎𝗍,𝖾𝖿𝖿𝖾𝖼𝗍𝗂𝗏𝖾,𝗂𝗇𝖺𝖼𝗍𝗂𝗏𝖾,𝖿𝗎𝗅𝖿𝗂𝗅𝗅𝖾𝖽,𝗏𝗂𝗈𝗅𝖺𝗍𝖾𝖽,𝗎𝗇𝗄𝗇𝗈𝗐𝗇⟩\.\\langle\\mathsf\{pending\},\\ \\mathsf\{out\},\\ \\mathsf\{effective\},\\ \\mathsf\{inactive\},\\ \\mathsf\{fulfilled\},\\ \\mathsf\{violated\},\\ \\mathsf\{unknown\}\\rangle\.A state atom𝗌𝗍𝖺𝗍𝖾​\(s,n\)\\mathsf\{state\}\(s,n\)states that rulennhas statess\.

###### Definition 1\(MONIR\-core expressions\)\.

The expressions of MONIR\-core are generated by

ℓ\\displaystyle\\ell::=p∣¬p,b::=ℓ∣𝗌𝗍𝖺𝗍𝖾\(s,n\),\\displaystyle:=p\\mid\\neg p,\\ b:=\\ell\\mid\\mathsf\{state\}\(s,n\),κ\\displaystyle\\kappa::=⊤∣ℓ∣κ1∧κ2∣𝖼𝗈𝗎𝗇𝗍\[l,u\]\(ℓ1,…,ℓm\),\\displaystyle:=\\top\\mid\\ell\\mid\\kappa\_\{1\}\\wedge\\kappa\_\{2\}\\mid\\mathsf\{count\}\_\{\[l,u\]\}\(\\ell\_\{1\},\\ldots,\\ell\_\{m\}\),α\\displaystyle\\alpha::=⊤∣κ∣𝗌𝗍𝖺𝗍𝖾\(s,n\)∣α1∧α2∣𝖼𝗈𝗎𝗇𝗍\[l,u\]\(b1,…,bm\),\\displaystyle:=\\top\\mid\\kappa\\mid\\mathsf\{state\}\(s,n\)\\mid\\alpha\_\{1\}\\wedge\\alpha\_\{2\}\\mid\\mathsf\{count\}\_\{\[l,u\]\}\(b\_\{1\},\\ldots,b\_\{m\}\),ω\\displaystyle\\omega::=M\(κ\)∣𝖾𝗑𝖾𝗆𝗉𝗍\(n\),ρ::=n:κ↝ℓ,r::=n:α⇒ω\.\\displaystyle:=M\(\\kappa\)\\mid\\mathsf\{exempt\}\(n\),\\rho:=n:\\kappa\\leadsto\\ell,r:=n:\\alpha\\Rightarrow\\omega\.Herep∈𝒫p\\in\\mathcal\{P\},n∈𝒩n\\in\\mathcal\{N\},s∈𝒮s\\in\\mathcal\{S\},M∈ℳM\\in\\mathcal\{M\}, and0≤l≤u≤m0\\leq l\\leq u\\leq m\. The expressionsppand¬p\\neg pare factual literals\. A factual formulaκ\\kappais state\-free and is used both as a proposition\-rule body and as a modalized target\. A normative conditionα\\alphamay additionally contain state atoms, which are used only to control normative\-rule applicability\.

For any expressionee, let𝖫𝗂𝗍​\(e\)\\mathsf\{Lit\}\(e\)be the set of factual literals occurring inee, let𝖠𝗍​\(e\)\\mathsf\{At\}\(e\)be the corresponding set of unsigned atoms, and let𝖲𝗍​\(e\)\\mathsf\{St\}\(e\)be the set of state atoms𝗌𝗍𝖺𝗍𝖾​\(s,n\)\\mathsf\{state\}\(s,n\)occurring inee\. For a ruleqqnamednn, let𝗂𝖽​\(q\)=n\\mathsf\{id\}\(q\)=n; for a rule setRR, let𝗂𝖽​\(R\)=\{𝗂𝖽​\(q\)∣q∈R\}\\mathsf\{id\}\(R\)=\\\{\\mathsf\{id\}\(q\)\\mid q\\in R\\\}\. For a proposition ruleρ=n:κ↝ℓ\\rho=n:\\kappa\\leadsto\\ell, let𝖻𝗈𝖽𝗒​\(ρ\)=κ\\mathsf\{body\}\(\\rho\)=\\kappaand𝗁𝖾𝖺𝖽​\(ρ\)=ℓ\\mathsf\{head\}\(\\rho\)=\\ell\. For a normative ruler=n:α⇒ωr=n:\\alpha\\Rightarrow\\omega, let𝖻𝗈𝖽𝗒​\(r\)=α\\mathsf\{body\}\(r\)=\\alphaand𝗈𝗎𝗍​\(r\)=ω\\mathsf\{out\}\(r\)=\\omega\.

###### Definition 2\(Rule base\)\.

A MONIR\-core rule base is a pairℬ=⟨RP,RN⟩\\mathcal\{B\}=\\langle R\_\{P\},R\_\{N\}\\rangle, whereRPR\_\{P\}is a finite set of proposition rules andRNR\_\{N\}is a finite set of normative rules\. We writeRℬ=RP∪RNR\_\{\\mathcal\{B\}\}=R\_\{P\}\\cup R\_\{N\}for the set of all rules inℬ\\mathcal\{B\}\. The rule baseℬ\\mathcal\{B\}is well formed if the following conditions hold\.

1. 1\.Rule identifiers are globally unique: for any distinctq,q′∈Rℬq,q^\{\\prime\}\\in R\_\{\\mathcal\{B\}\},𝗂𝖽​\(q\)≠𝗂𝖽​\(q′\)\\mathsf\{id\}\(q\)\\neq\\mathsf\{id\}\(q^\{\\prime\}\)\.
2. 2\.Every state atom refers to a normative rule: if𝗌𝗍𝖺𝗍𝖾​\(s,n\)\\mathsf\{state\}\(s,n\)occurs inℬ\\mathcal\{B\}, thenn∈𝗂𝖽​\(RN\)n\\in\\mathsf\{id\}\(R\_\{N\}\)\.
3. 3\.Every exemption refers to a normative rule: if𝖾𝗑𝖾𝗆𝗉𝗍​\(n\)\\mathsf\{exempt\}\(n\)occurs inℬ\\mathcal\{B\}, thenn∈𝗂𝖽​\(RN\)n\\in\\mathsf\{id\}\(R\_\{N\}\)\.

### Operational Semantics

MONIR\-core is given an operational semantics in stages\. It first fixes the three\-valued evaluation of conditions, then defines the successive semantic constructions used to derive rule outputs, conflicts, and compliance status\.

Let𝕍3=\{𝐭,𝐟,𝐮\}\\mathbb\{V\}\_\{3\}=\\\{\\mathbf\{t\},\\mathbf\{f\},\\mathbf\{u\}\\\}\. For a finite setAAof auxiliary atoms, letℒ3​\(A\)\\mathcal\{L\}\_\{3\}\(A\)be the formula language overAAwith⊤\\top,⊥\\bot,¬\\neg,∧\\wedge, and∨\\vee\. A valuation is a mapν:A→𝕍3\\nu:A\\to\\mathbb\{V\}\_\{3\}\.

###### Definition 3\(Regular three\-valued evaluator\)\.

A regular three\-valued evaluator is a family of maps

ηA:ℒ3​\(A\)×\(A→𝕍3\)→𝕍3\\eta\_\{A\}:\\mathcal\{L\}\_\{3\}\(A\)\\times\(A\\to\\mathbb\{V\}\_\{3\}\)\\to\\mathbb\{V\}\_\{3\}such that eachηA\\eta\_\{A\}is total, deterministic, extensional, truth\-functional, classically conservative on bivalent valuations, preserves unknown under negation, and is polynomial\-time computable\. Truth\-functionality means that there are fixed truth functions for¬\\neg,∧\\wedge, and∨\\veeused compositionally by everyηA\\eta\_\{A\}\. In particular,

¬𝐭=𝐟,¬𝐟=𝐭,¬𝐮=𝐮\.\\neg\\mathbf\{t\}=\\mathbf\{f\},\\quad\\neg\\mathbf\{f\}=\\mathbf\{t\},\\quad\\neg\\mathbf\{u\}=\\mathbf\{u\}\.

All semantic definitions are parameterized by a fixed regular evaluatorη\\eta\. Strong Kleene evaluation\(Kleene[1952](https://arxiv.org/html/2606.04619#bib.bib18)\)is used as the default evaluator in the examples and experiments\. We omit the subscriptAAinηA\\eta\_\{A\}when the auxiliary atom set is clear\.

A translation⟦⋅⟧X\\llbracket\\cdot\\rrbracket\_\{X\}maps expressions of syntactic categoryXXintoℒ3​\(A\)\\mathcal\{L\}\_\{3\}\(A\)\. For a compatible valuationν\\nu, write

νX\(e\)=η\(⟦e⟧X,ν\)\.\\nu^\{X\}\(e\)=\\eta\(\\llbracket e\\rrbracket\_\{X\},\\nu\)\.The shared translation cases are

⟦⊤⟧X=⊤,⟦p⟧X=p,⟦¬p⟧X=¬p,\\displaystyle\\llbracket\\top\\rrbracket\_\{X\}=\\top,\\quad\\llbracket p\\rrbracket\_\{X\}=p,\\quad\\llbracket\\neg p\\rrbracket\_\{X\}=\\neg p,⟦φ1∧φ2⟧X=⟦φ1⟧X∧⟦φ2⟧X\.\\displaystyle\\llbracket\\varphi\_\{1\}\\wedge\\varphi\_\{2\}\\rrbracket\_\{X\}=\\llbracket\\varphi\_\{1\}\\rrbracket\_\{X\}\\wedge\\llbracket\\varphi\_\{2\}\\rrbracket\_\{X\}\.Here¬p\\neg pis translated as formula negation overppand is evaluated by the fixedη\\eta; it is not a separate unsigned atom\.

Letx→=\(x1,…,xm\)\\vec\{x\}=\(x\_\{1\},\\ldots,x\_\{m\}\), let\[m\]=\{1,…,m\}\[m\]=\\\{1,\\ldots,m\\\}, and let𝒞km=\{J⊆\[m\]∣\|J\|=k\}\\mathcal\{C\}\_\{k\}^\{m\}=\\\{J\\subseteq\[m\]\\mid\|J\|=k\\\}\. For any translation⟦⋅⟧X\\llbracket\\cdot\\rrbracket\_\{X\}, define

𝖠𝗍𝖫𝖾𝖺𝗌𝗍kX\(x→\)=∨J∈𝒞km∧j∈J⟦xj⟧Xfor1≤k≤m,\\displaystyle\\mathsf\{AtLeast\}^\{X\}\_\{k\}\(\\vec\{x\}\)=\\vee\_\{J\\in\\mathcal\{C\}\_\{k\}^\{m\}\}\\wedge\_\{j\\in J\}\\llbracket x\_\{j\}\\rrbracket\_\{X\}\\text\{ for \}1\\leq k\\leq m,𝖠𝗍𝖫𝖾𝖺𝗌𝗍0X​\(x→\)=⊤,𝖠𝗍𝖫𝖾𝖺𝗌𝗍kX​\(x→\)=⊥for​k\>m,\\displaystyle\\mathsf\{AtLeast\}^\{X\}\_\{0\}\(\\vec\{x\}\)=\\top,\\quad\\mathsf\{AtLeast\}^\{X\}\_\{k\}\(\\vec\{x\}\)=\\bot\\text\{ for \}k\>m,𝖢𝖺𝗋𝖽\[l,u\]X​\(x→\)=𝖠𝗍𝖫𝖾𝖺𝗌𝗍lX​\(x→\)∧¬𝖠𝗍𝖫𝖾𝖺𝗌𝗍u\+1X​\(x→\)\.\\displaystyle\\mathsf\{Card\}^\{X\}\_\{\[l,u\]\}\(\\vec\{x\}\)=\\mathsf\{AtLeast\}^\{X\}\_\{l\}\(\\vec\{x\}\)\\wedge\\neg\\mathsf\{AtLeast\}^\{X\}\_\{u\+1\}\(\\vec\{x\}\)\.Cardinality has no separate counting semantics in MONIR\-core\. Its value is the value assigned by the fixed evaluatorη\\etato the explicit𝖠𝗍𝖫𝖾𝖺𝗌𝗍\\mathsf\{AtLeast\}translation\. Thus, different regular evaluators may induce different unknown\-propagation policies for cardinality\.

An input interpretation over𝒫\\mathcal\{P\}is a pairI=⟨I\+,I−⟩I=\\langle I^\{\+\},I^\{\-\}\\ranglewithI\+∩I−=∅I^\{\+\}\\cap I^\{\-\}=\\emptyset\. It induces

νI​\(p\)=\{𝐭p∈I\+,𝐟p∈I−,𝐮p∉I\+∪I−\.\\nu\_\{I\}\(p\)=\\begin\{cases\}\\mathbf\{t\}&p\\in I^\{\+\},\\\\ \\mathbf\{f\}&p\\in I^\{\-\},\\\\ \\mathbf\{u\}&p\\notin I^\{\+\}\\cup I^\{\-\}\.\\end\{cases\}
###### Definition 4\(Admissible rule base\)\.

Letℬ=⟨RP,RN⟩\\mathcal\{B\}=\\langle R\_\{P\},R\_\{N\}\\ranglebe a well\-formed MONIR\-core rule base\. The rule baseℬ\\mathcal\{B\}is admissible if there exist mappingsλP:RP→ℕ\\lambda\_\{P\}:R\_\{P\}\\to\\mathbb\{N\}andλN:RN→ℕ\\lambda\_\{N\}:R\_\{N\}\\to\\mathbb\{N\}such that the following conditions hold\.

1. 1\.\(F\-Stratification\) For allρ,ρ′∈RP\\rho,\\rho^\{\\prime\}\\in R\_\{P\}, if𝖠𝗍​\(𝗁𝖾𝖺𝖽​\(ρ′\)\)∩𝖠𝗍​\(𝖻𝗈𝖽𝗒​\(ρ\)\)≠∅\\mathsf\{At\}\(\\mathsf\{head\}\(\\rho^\{\\prime\}\)\)\\cap\\mathsf\{At\}\(\\mathsf\{body\}\(\\rho\)\)\\neq\\emptyset, thenλP​\(ρ′\)<λP​\(ρ\)\\lambda\_\{P\}\(\\rho^\{\\prime\}\)<\\lambda\_\{P\}\(\\rho\)\.
2. 2\.\(N\-Stratification\) For allr,r′∈RNr,r^\{\\prime\}\\in R\_\{N\}, if𝗌𝗍𝖺𝗍𝖾​\(s,𝗂𝖽​\(r′\)\)∈𝖲𝗍​\(𝖻𝗈𝖽𝗒​\(r\)\)\\mathsf\{state\}\(s,\\mathsf\{id\}\(r^\{\\prime\}\)\)\\in\\mathsf\{St\}\(\\mathsf\{body\}\(r\)\)for somes∈𝒮s\\in\\mathcal\{S\}, thenλN​\(r′\)<λN​\(r\)\\lambda\_\{N\}\(r^\{\\prime\}\)<\\lambda\_\{N\}\(r\)\.
3. 3\.\(E\-Admissibility\) For allr,r′∈RNr,r^\{\\prime\}\\in R\_\{N\}, if𝗈𝗎𝗍​\(r\)=𝖾𝗑𝖾𝗆𝗉𝗍​\(𝗂𝖽​\(r′\)\)\\mathsf\{out\}\(r\)=\\mathsf\{exempt\}\(\\mathsf\{id\}\(r^\{\\prime\}\)\), thenλN​\(r\)<λN​\(r′\)\\lambda\_\{N\}\(r\)<\\lambda\_\{N\}\(r^\{\\prime\}\)\.

F\-Stratification prevents proposition\-rule bodies from depending on facts derived in the same or later factual strata\. N\-Stratification makes state\-dependent normative rules read only states fixed in lower normative strata\. E\-Admissibility enforces non\-retroactive exemption: an exemption must be generated before the target rule is evaluated\.

The factual translation⟦⋅⟧F\\llbracket\\cdot\\rrbracket\_\{F\}extends the shared cases by

⟦𝖼𝗈𝗎𝗇𝗍\[l,u\]\(ℓ1,…,ℓm\)⟧F=𝖢𝖺𝗋𝖽\[l,u\]F\(ℓ1,…,ℓm\)\.\\llbracket\\mathsf\{count\}\_\{\[l,u\]\}\(\\ell\_\{1\},\\ldots,\\ell\_\{m\}\)\\rrbracket\_\{F\}=\\mathsf\{Card\}^\{F\}\_\{\[l,u\]\}\(\\ell\_\{1\},\\ldots,\\ell\_\{m\}\)\.The factual value ofκ\\kappaunderIIis written as

νIF\(κ\)=η\(⟦κ⟧F,νI\)\.\\nu\_\{I\}^\{F\}\(\\kappa\)=\\eta\(\\llbracket\\kappa\\rrbracket\_\{F\},\\nu\_\{I\}\)\.
###### Definition 5\(Factual closure\)\.

Letℬ=⟨RP,RN⟩\\mathcal\{B\}=\\langle R\_\{P\},R\_\{N\}\\ranglebe admissible, letIIbe an input interpretation, and fix a witnessing factual stratificationλP\\lambda\_\{P\}\. For each occupied stratumkk, in increasing order, set

RPk=\{ρ∈RP∣λP​\(ρ\)=k\}\.R\_\{P\}^\{k\}=\\\{\\rho\\in R\_\{P\}\\mid\\lambda\_\{P\}\(\\rho\)=k\\\}\.For the first occupied stratum, letI<k=II\_\{<k\}=I\. For any later occupied stratum, letI<kI\_\{<k\}be the interpretation obtained after processing all occupied strata belowkk\. Define

Dk=\{𝗁𝖾𝖺𝖽​\(ρ\)∣ρ∈RPk,νI<kF​\(𝖻𝗈𝖽𝗒​\(ρ\)\)=𝐭\}\.D\_\{k\}=\\\{\\mathsf\{head\}\(\\rho\)\\mid\\rho\\in R\_\{P\}^\{k\},\\ \\nu\_\{I\_\{<k\}\}^\{F\}\(\\mathsf\{body\}\(\\rho\)\)=\\mathbf\{t\}\\\}\.Let

Dk\+=Dk∩𝒫,Dk−=\{p∈𝒫∣¬p∈Dk\},\\displaystyle D\_\{k\}^\{\+\}=D\_\{k\}\\cap\\mathcal\{P\},\\quad D\_\{k\}^\{\-\}=\\\{p\\in\\mathcal\{P\}\\mid\\neg p\\in D\_\{k\}\\\},I≤k=⟨I<k\+∪Dk\+,I<k−∪Dk−⟩\.\\displaystyle I\_\{\\leq k\}=\\langle I\_\{<k\}^\{\+\}\\cup D\_\{k\}^\{\+\},I\_\{<k\}^\{\-\}\\cup D\_\{k\}^\{\-\}\\rangle\.IfI≤k\+∩I≤k−≠∅I\_\{\\leq k\}^\{\+\}\\cap I\_\{\\leq k\}^\{\-\}\\neq\\emptysetfor somekk, the factual closure is undefined\. Otherwise, the final interpretation after all factual strata is the factual closureI∗I^\{\\ast\}\.

###### Lemma 1\(Factual\-body invariance\)\.

LetI∗I^\{\\ast\}be the factual closure ofII, and letρ∈RP\\rho\\in R\_\{P\}withk=λP​\(ρ\)k=\\lambda\_\{P\}\(\\rho\)\. Then

νI<kF​\(𝖻𝗈𝖽𝗒​\(ρ\)\)=νI∗F​\(𝖻𝗈𝖽𝗒​\(ρ\)\)\.\\nu\_\{I\_\{<k\}\}^\{F\}\(\\mathsf\{body\}\(\\rho\)\)=\\nu\_\{I^\{\\ast\}\}^\{F\}\(\\mathsf\{body\}\(\\rho\)\)\.

###### Proof sketch\.

By F\-Stratification, each body atom is either exogenous and fixed byII, or defined by a proposition rule in a lower factual stratum\. Later proposition rules cannot change its value\. ∎

A normative condition is evaluated from the factual closure and the rule states fixed in lower normative strata\. For a normative rule setRNR\_\{N\}, a state context is a set

Σ⊆\{𝗌𝗍𝖺𝗍𝖾​\(s,n\)∣s∈𝒮,n∈𝗂𝖽​\(RN\)\}\.\\Sigma\\subseteq\\\{\\mathsf\{state\}\(s,n\)\\mid s\\in\\mathcal\{S\},\\ n\\in\\mathsf\{id\}\(R\_\{N\}\)\\\}\.The contexts produced by staged evaluation are functional:

𝗌𝗍𝖺𝗍𝖾​\(s,n\)∈Σ​and​𝗌𝗍𝖺𝗍𝖾​\(s′,n\)∈Σ⇒s=s′\.\\mathsf\{state\}\(s,n\)\\in\\Sigma\\text\{ and \}\\mathsf\{state\}\(s^\{\\prime\},n\)\\in\\Sigma\\Rightarrow s=s^\{\\prime\}\.
Given an interpretationIIand a state contextΣ\\Sigma, factual atoms are read fromII:

νI,Σα​\(p\)=νI​\(p\)\.\\nu\_\{I,\\Sigma\}^\{\\alpha\}\(p\)=\\nu\_\{I\}\(p\)\.State atoms are read fromΣ\\Sigmaby

νI,Σα​\(𝗌𝗍𝖺𝗍𝖾​\(s,n\)\)=\{𝐭𝗌𝗍𝖺𝗍𝖾​\(s,n\)∈Σ,𝐟𝗌𝗍𝖺𝗍𝖾​\(s′,n\)∈Σ​for some​s′≠s,𝐮𝗌𝗍𝖺𝗍𝖾​\(s′,n\)∉Σ​for all​s′∈𝒮\.\\nu\_\{I,\\Sigma\}^\{\\alpha\}\(\\mathsf\{state\}\(s,n\)\)=\\begin\{cases\}\\mathbf\{t\}&\\mathsf\{state\}\(s,n\)\\in\\Sigma,\\\\ \\mathbf\{f\}&\\mathsf\{state\}\(s^\{\\prime\},n\)\\in\\Sigma\\text\{ for some \}s^\{\\prime\}\\neq s,\\\\ \\mathbf\{u\}&\\mathsf\{state\}\(s^\{\\prime\},n\)\\notin\\Sigma\\text\{ for all \}s^\{\\prime\}\\in\\mathcal\{S\}\.\\end\{cases\}Thus, if rulennhas no fixed state inΣ\\Sigma, its state tests are unknown\.

The normative translation⟦⋅⟧N\\llbracket\\cdot\\rrbracket\_\{N\}extends the shared cases by

⟦𝗌𝗍𝖺𝗍𝖾\(s,n\)⟧N\\displaystyle\\llbracket\\mathsf\{state\}\(s,n\)\\rrbracket\_\{N\}=𝗌𝗍𝖺𝗍𝖾​\(s,n\),\\displaystyle=\\mathsf\{state\}\(s,n\),⟦𝖼𝗈𝗎𝗇𝗍\[l,u\]\(b1,…,bm\)⟧N\\displaystyle\\llbracket\\mathsf\{count\}\_\{\[l,u\]\}\(b\_\{1\},\\ldots,b\_\{m\}\)\\rrbracket\_\{N\}=𝖢𝖺𝗋𝖽\[l,u\]N​\(b1,…,bm\)\.\\displaystyle=\\mathsf\{Card\}^\{N\}\_\{\[l,u\]\}\(b\_\{1\},\\ldots,b\_\{m\}\)\.The value ofα\\alphaunderIIandΣ\\Sigmais

νI,ΣN\(α\)=η\(⟦α⟧N,νI,Σα\)\.\\nu\_\{I,\\Sigma\}^\{N\}\(\\alpha\)=\\eta\(\\llbracket\\alpha\\rrbracket\_\{N\},\\nu\_\{I,\\Sigma\}^\{\\alpha\}\)\.During normative evaluation, modal targets are evaluated byνI∗F\\nu\_\{I^\{\\ast\}\}^\{F\}\. ForM∈\{𝖮,𝖥\}M\\in\\\{\\mathsf\{O\},\\mathsf\{F\}\\\}andv∈𝕍3v\\in\\mathbb\{V\}\_\{3\}, define

τ​\(M,v\)=\{𝖿𝗎𝗅𝖿𝗂𝗅𝗅𝖾𝖽\(M,v\)∈\{\(𝖮,𝐭\),\(𝖥,𝐟\)\},𝗏𝗂𝗈𝗅𝖺𝗍𝖾𝖽\(M,v\)∈\{\(𝖮,𝐟\),\(𝖥,𝐭\)\},𝗎𝗇𝗄𝗇𝗈𝗐𝗇v=𝐮\.\\tau\(M,v\)=\\begin\{cases\}\\mathsf\{fulfilled\}&\(M,v\)\\in\\\{\(\\mathsf\{O\},\\mathbf\{t\}\),\(\\mathsf\{F\},\\mathbf\{f\}\)\\\},\\\\ \\mathsf\{violated\}&\(M,v\)\\in\\\{\(\\mathsf\{O\},\\mathbf\{f\}\),\(\\mathsf\{F\},\\mathbf\{t\}\)\\\},\\\\ \\mathsf\{unknown\}&v=\\mathbf\{u\}\.\\end\{cases\}Recommendations and negative recommendations are not evaluated as fulfilled or violated at this stage; they enter only the soft aggregate view\.

###### Definition 6\(Normative evaluation\)\.

Letℬ=⟨RP,RN⟩\\mathcal\{B\}=\\langle R\_\{P\},R\_\{N\}\\ranglebe admissible, letI∗I^\{\\ast\}be the factual closure ofII, and fix a witnessing normative stratificationλN\\lambda\_\{N\}\. For each occupied stratumkk, in increasing order, set

RNk=\{r∈RN∣λN​\(r\)=k\}\.R\_\{N\}^\{k\}=\\\{r\\in R\_\{N\}\\mid\\lambda\_\{N\}\(r\)=k\\\}\.AssumingΣj\\Sigma\_\{j\}andGjG\_\{j\}have been defined for all occupied strataj<kj<k, let

Σ<k=⋃j<kΣj,G<k=⋃j<kGj,\\displaystyle\\Sigma\_\{<k\}=\\bigcup\_\{j<k\}\\Sigma\_\{j\},\\quad G\_\{<k\}=\\bigcup\_\{j<k\}G\_\{j\},E<k=\{n∣\(m,𝖾𝗑𝖾𝗆𝗉𝗍​\(n\)\)∈G<k\}\.\\displaystyle E\_\{<k\}=\\\{n\\mid\(m,\\mathsf\{exempt\}\(n\)\)\\in G\_\{<k\}\\\}\.If there is no lower stratum, these sets are empty\.

Forr∈RNkr\\in R\_\{N\}^\{k\}, write

βk​\(r\)=νI∗,Σ<kN​\(𝖻𝗈𝖽𝗒​\(r\)\)\.\\beta\_\{k\}\(r\)=\\nu\_\{I^\{\\ast\},\\Sigma\_\{<k\}\}^\{N\}\(\\mathsf\{body\}\(r\)\)\.The generated outputs at stratumkkare

Gk=\{\(𝗂𝖽​\(r\),𝗈𝗎𝗍​\(r\)\)∣r∈RNk,βk​\(r\)=𝐭,𝗂𝖽​\(r\)∉E<k\}\.G\_\{k\}=\\\{\(\\mathsf\{id\}\(r\),\\mathsf\{out\}\(r\)\)\\mid r\\in R\_\{N\}^\{k\},\\ \\beta\_\{k\}\(r\)=\\mathbf\{t\},\\ \\mathsf\{id\}\(r\)\\notin E\_\{<k\}\\\}\.
Forr∈RNkr\\in R\_\{N\}^\{k\}, define

σk​\(r\)=\{𝗈𝗎𝗍βk​\(r\)=𝐟,𝗉𝖾𝗇𝖽𝗂𝗇𝗀βk​\(r\)=𝐮,𝗂𝗇𝖺𝖼𝗍𝗂𝗏𝖾βk​\(r\)=𝐭,𝗂𝖽​\(r\)∈E<k,τ​\(M,νI∗F​\(κ\)\)βk​\(r\)=𝐭,𝗂𝖽​\(r\)∉E<k,𝗈𝗎𝗍​\(r\)=M​\(κ\),M∈\{𝖮,𝖥\},𝖾𝖿𝖿𝖾𝖼𝗍𝗂𝗏𝖾βk​\(r\)=𝐭,𝗂𝖽​\(r\)∉E<k,𝗈𝗎𝗍​\(r\)=M​\(κ\),M∈\{𝖯,𝖱,𝖭𝖱\},𝖾𝖿𝖿𝖾𝖼𝗍𝗂𝗏𝖾βk​\(r\)=𝐭,𝗂𝖽​\(r\)∉E<k,𝗈𝗎𝗍​\(r\)=𝖾𝗑𝖾𝗆𝗉𝗍​\(n\)\.\\sigma\_\{k\}\(r\)=\\begin\{cases\}\\mathsf\{out\}&\\beta\_\{k\}\(r\)=\\mathbf\{f\},\\\\ \\mathsf\{pending\}&\\beta\_\{k\}\(r\)=\\mathbf\{u\},\\\\ \\mathsf\{inactive\}&\\beta\_\{k\}\(r\)=\\mathbf\{t\},\\ \\mathsf\{id\}\(r\)\\in E\_\{<k\},\\\\ \\tau\(M,\\nu\_\{I^\{\\ast\}\}^\{F\}\(\\kappa\)\)&\\begin\{array\}\[t\]\{l\}\\beta\_\{k\}\(r\)=\\mathbf\{t\},\\ \\mathsf\{id\}\(r\)\\notin E\_\{<k\},\\\\ \\mathsf\{out\}\(r\)=M\(\\kappa\),\\ M\\in\\\{\\mathsf\{O\},\\mathsf\{F\}\\\},\\end\{array\}\\\\ \\mathsf\{effective\}&\\begin\{array\}\[t\]\{l\}\\beta\_\{k\}\(r\)=\\mathbf\{t\},\\ \\mathsf\{id\}\(r\)\\notin E\_\{<k\},\\\\ \\mathsf\{out\}\(r\)=M\(\\kappa\),\\ M\\in\\\{\\mathsf\{P\},\\mathsf\{R\},\\mathsf\{NR\}\\\},\\end\{array\}\\\\ \\mathsf\{effective\}&\\begin\{array\}\[t\]\{l\}\\beta\_\{k\}\(r\)=\\mathbf\{t\},\\ \\mathsf\{id\}\(r\)\\notin E\_\{<k\},\\\\ \\mathsf\{out\}\(r\)=\\mathsf\{exempt\}\(n\)\.\\end\{array\}\\end\{cases\}Then

Σk=\{𝗌𝗍𝖺𝗍𝖾​\(σk​\(r\),𝗂𝖽​\(r\)\)∣r∈RNk\}\.\\Sigma\_\{k\}=\\\{\\mathsf\{state\}\(\\sigma\_\{k\}\(r\),\\mathsf\{id\}\(r\)\)\\mid r\\in R\_\{N\}^\{k\}\\\}\.After all strata are processed, let

Σ∗\\displaystyle\\Sigma^\{\\ast\}=⋃kΣk,\\displaystyle=\\bigcup\_\{k\}\\Sigma\_\{k\},G∗\\displaystyle G^\{\\ast\}=⋃kGk\.\\displaystyle=\\bigcup\_\{k\}G\_\{k\}\.The pair⟨Σ∗,G∗⟩\\langle\\Sigma^\{\\ast\},G^\{\\ast\}\\rangleis the result of normative evaluation\.

###### Proposition 2\(Normative determinacy and output traceability\)\.

Let⟨Σ∗,G∗⟩\\langle\\Sigma^\{\\ast\},G^\{\\ast\}\\ranglebe the result of normative evaluation\. Then the following properties hold\.

1. 1\.For everyn∈𝗂𝖽​\(RN\)n\\in\\mathsf\{id\}\(R\_\{N\}\), there is a uniques∈𝒮s\\in\\mathcal\{S\}such that𝗌𝗍𝖺𝗍𝖾​\(s,n\)∈Σ∗\\mathsf\{state\}\(s,n\)\\in\\Sigma^\{\\ast\}\.
2. 2\.For every\(n,ω\)∈G∗\(n,\\omega\)\\in G^\{\\ast\}, there is a unique ruler∈RNr\\in R\_\{N\}such that, fork=λN​\(r\)k=\\lambda\_\{N\}\(r\), 𝗂𝖽​\(r\)=n,𝗈𝗎𝗍​\(r\)=ω,\\displaystyle\\mathsf\{id\}\(r\)=n,\\quad\\mathsf\{out\}\(r\)=\\omega,νI∗,Σ<kN​\(𝖻𝗈𝖽𝗒​\(r\)\)=𝐭,n∉E<k\.\\displaystyle\\nu^\{N\}\_\{I^\{\\ast\},\\Sigma\_\{<k\}\}\(\\mathsf\{body\}\(r\)\)=\\mathbf\{t\},\\quad n\\notin E\_\{<k\}\.

###### Proof sketch\.

For item 1, each normative rule occurs in exactly one stratum and receives exactly one state by the definition ofσk\\sigma\_\{k\}\. Since rule identifiers are globally unique, no other rule can contribute a state atom with the same identifier\. For item 2, every element ofG∗G^\{\\ast\}belongs to someGkG\_\{k\}\. By the definition ofGkG\_\{k\}, it is generated by a rule whose body is true and whose identifier is not exempted by lower strata\. Global uniqueness of rule identifiers gives uniqueness of that rule\. ∎

###### Proposition 3\(Exemption discipline\)\.

Letr∈RNr\\in R\_\{N\},n=𝗂𝖽​\(r\)n=\\mathsf\{id\}\(r\), andk=λN​\(r\)k=\\lambda\_\{N\}\(r\)\. If𝗌𝗍𝖺𝗍𝖾​\(𝗂𝗇𝖺𝖼𝗍𝗂𝗏𝖾,n\)∈Σ∗\\mathsf\{state\}\(\\mathsf\{inactive\},n\)\\in\\Sigma^\{\\ast\}, then:

1. 1\.there is no\(n,ω\)∈G∗\(n,\\omega\)\\in G^\{\\ast\};
2. 2\.there exists\(m,𝖾𝗑𝖾𝗆𝗉𝗍​\(n\)\)∈G<k\(m,\\mathsf\{exempt\}\(n\)\)\\in G\_\{<k\};
3. 3\.every generated exemption ofnnis generated beforerris evaluated\.

###### Proof sketch\.

The state𝗂𝗇𝖺𝖼𝗍𝗂𝗏𝖾\\mathsf\{inactive\}arises only whenνI∗,Σ<kN​\(𝖻𝗈𝖽𝗒​\(r\)\)=𝐭\\nu^\{N\}\_\{I^\{\\ast\},\\Sigma\_\{<k\}\}\(\\mathsf\{body\}\(r\)\)=\\mathbf\{t\}andn∈E<kn\\in E\_\{<k\}\. Hencerris excluded fromGkG\_\{k\}, andn∈E<kn\\in E\_\{<k\}gives a lower\-stratum exemption witness\. The last item follows from E\-Admissibility\. ∎

###### Lemma 4\(Normative\-state invariance\)\.

Let⟨Σ∗,G∗⟩\\langle\\Sigma^\{\\ast\},G^\{\\ast\}\\ranglebe the result of normative evaluation, and letr∈RNr\\in R\_\{N\}withk=λN​\(r\)k=\\lambda\_\{N\}\(r\)\. Then

νI∗,Σ<kN​\(𝖻𝗈𝖽𝗒​\(r\)\)=νI∗,Σ∗N​\(𝖻𝗈𝖽𝗒​\(r\)\)\.\\nu\_\{I^\{\\ast\},\\Sigma\_\{<k\}\}^\{N\}\(\\mathsf\{body\}\(r\)\)=\\nu\_\{I^\{\\ast\},\\Sigma^\{\\ast\}\}^\{N\}\(\\mathsf\{body\}\(r\)\)\.

###### Proof sketch\.

Analogous to Lemma[1](https://arxiv.org/html/2606.04619#Thmtheorem1), using N\-Stratification instead of F\-Stratification\. ∎

Aggregation interprets active modal outputs as hard obligations, soft obligations, and explicit permissions\. A signed target\+κ\+\\kappasupportsκ\\kappa, while−κ\-\\kappasupports avoidingκ\\kappa:

𝖮​\(κ\)\\displaystyle\\mathsf\{O\}\(\\kappa\)↦𝖧𝖺𝗋𝖽​\(\+κ\),\\displaystyle\\mapsto\\mathsf\{Hard\}\(\+\\kappa\),𝖥​\(κ\)\\displaystyle\\mathsf\{F\}\(\\kappa\)↦𝖧𝖺𝗋𝖽​\(−κ\),\\displaystyle\\mapsto\\mathsf\{Hard\}\(\-\\kappa\),𝖯​\(κ\)\\displaystyle\\mathsf\{P\}\(\\kappa\)↦𝖯𝖾𝗋𝗆​\(\+κ\),\\displaystyle\\mapsto\\mathsf\{Perm\}\(\+\\kappa\),𝖱​\(κ\)\\displaystyle\\mathsf\{R\}\(\\kappa\)↦𝖲𝗈𝖿𝗍​\(\+κ\),\\displaystyle\\mapsto\\mathsf\{Soft\}\(\+\\kappa\),𝖭𝖱​\(κ\)\\displaystyle\\mathsf\{NR\}\(\\kappa\)↦𝖲𝗈𝖿𝗍​\(−κ\)\.\\displaystyle\\mapsto\\mathsf\{Soft\}\(\-\\kappa\)\.These are aggregation\-level views, not source\-language modalities\. In particular, permissions are explicit outputs; they do not stand for the absence of hard obligations\.

Let⟂O\\perp\_\{O\}be a fixed symmetric incompatibility relation on signed targets, including\+κ⟂O−κ\+\\kappa\\perp\_\{O\}\-\\kappafor every factual targetκ\\kappa, and\+p⟂O\+\(¬p\)\+p\\perp\_\{O\}\+\(\\neg p\)and−p⟂O−\(¬p\)\-p\\perp\_\{O\}\-\(\\neg p\)for each atompp\. Additional domain\-specific incompatibilities may be added\. The relation is used only in aggregation\. It is syntactic or declared: MONIR\-core does not infer all semantic incompatibilities between factual targets unless they are represented in⟂O\\perp\_\{O\}or introduced by a target\-normalization procedure\.

For setsX,YX,Yof named signed targets, define

𝖢𝗈𝗇𝖿∗\(X,Y\)=\{\\displaystyle\\mathsf\{Conf\}^\{\\ast\}\(X,Y\)=\\\{\{n,n′\}∣\(n,χ\)∈X,\(n′,χ′\)∈Y,\\displaystyle\\\{n,n^\{\\prime\}\\\}\\mid\(n,\\chi\)\\in X,\\ \(n^\{\\prime\},\\chi^\{\\prime\}\)\\in Y,n≠n′,χ⟂Oχ′\}\.\\displaystyle n\\neq n^\{\\prime\},\\ \\chi\\perp\_\{O\}\\chi^\{\\prime\}\\\}\.Write𝖢𝗈𝗇𝖿∗​\(X\)\\mathsf\{Conf\}^\{\\ast\}\(X\)for𝖢𝗈𝗇𝖿∗​\(X,X\)\\mathsf\{Conf\}^\{\\ast\}\(X,X\)\.

###### Definition 7\(Aggregated output\)\.

Assume thatI∗I^\{\\ast\}is defined and normative evaluation yields⟨Σ∗,G∗⟩\\langle\\Sigma^\{\\ast\},G^\{\\ast\}\\rangle; otherwise𝖮𝗎𝗍ℬη​\(I\)\\mathsf\{Out\}^\{\\eta\}\_\{\\mathcal\{B\}\}\(I\)is undefined\. We write𝖮𝗎𝗍​\(I\)\\mathsf\{Out\}\(I\)whenη\\etaandℬ\\mathcal\{B\}are fixed\.

The active hard obligations, soft obligations, and permissions are represented by

𝖧𝖺𝗋𝖽∗=\\displaystyle\\mathsf\{Hard\}^\{\\ast\}=\{\}\{\(n,\+κ\)∣\(n,𝖮​\(κ\)\)∈G∗\}\\displaystyle\\\{\(n,\+\\kappa\)\\mid\(n,\\mathsf\{O\}\(\\kappa\)\)\\in G^\{\\ast\}\\\}∪\{\(n,−κ\)∣\(n,𝖥​\(κ\)\)∈G∗\},\\displaystyle\\cup\\\{\(n,\-\\kappa\)\\mid\(n,\\mathsf\{F\}\(\\kappa\)\)\\in G^\{\\ast\}\\\},𝖲𝗈𝖿𝗍∗=\\displaystyle\\mathsf\{Soft\}^\{\\ast\}=\{\}\{\(n,\+κ\)∣\(n,𝖱​\(κ\)\)∈G∗\}\\displaystyle\\\{\(n,\+\\kappa\)\\mid\(n,\\mathsf\{R\}\(\\kappa\)\)\\in G^\{\\ast\}\\\}∪\{\(n,−κ\)∣\(n,𝖭𝖱​\(κ\)\)∈G∗\},\\displaystyle\\cup\\\{\(n,\-\\kappa\)\\mid\(n,\\mathsf\{NR\}\(\\kappa\)\)\\in G^\{\\ast\}\\\},𝖯𝖾𝗋𝗆∗=\\displaystyle\\mathsf\{Perm\}^\{\\ast\}=\{\}\{\(n,\+κ\)∣\(n,𝖯​\(κ\)\)∈G∗\}\.\\displaystyle\\\{\(n,\+\\kappa\)\\mid\(n,\\mathsf\{P\}\(\\kappa\)\)\\in G^\{\\ast\}\\\}\.
Soft obligations already present as hard obligations are ignored in soft\-conflict checking:

𝖲𝗈𝖿𝗍0∗=\{\(n,χ\)∈𝖲𝗈𝖿𝗍∗∣\(m,χ\)∉𝖧𝖺𝗋𝖽∗​for all​m\}\.\\mathsf\{Soft\}^\{\\ast\}\_\{0\}=\\\{\(n,\\chi\)\\in\\mathsf\{Soft\}^\{\\ast\}\\mid\(m,\\chi\)\\notin\\mathsf\{Hard\}^\{\\ast\}\\text\{ for all \}m\\\}\.This absorption is syntactic unless a separate target\-equivalence relation is specified\.

Hard conflicts include hard\-hard conflicts and hard\-permission conflicts; soft conflicts involve only unabsorbed soft obligations:

𝖧𝖢∗\\displaystyle\\mathsf\{HC\}^\{\\ast\}=𝖢𝗈𝗇𝖿∗​\(𝖧𝖺𝗋𝖽∗\)∪𝖢𝗈𝗇𝖿∗​\(𝖧𝖺𝗋𝖽∗,𝖯𝖾𝗋𝗆∗\),\\displaystyle=\\mathsf\{Conf\}^\{\\ast\}\(\\mathsf\{Hard\}^\{\\ast\}\)\\cup\\mathsf\{Conf\}^\{\\ast\}\(\\mathsf\{Hard\}^\{\\ast\},\\mathsf\{Perm\}^\{\\ast\}\),𝖲𝖢∗\\displaystyle\\mathsf\{SC\}^\{\\ast\}=𝖢𝗈𝗇𝖿∗​\(𝖧𝖺𝗋𝖽∗,𝖲𝗈𝖿𝗍0∗\)∪𝖢𝗈𝗇𝖿∗​\(𝖲𝗈𝖿𝗍0∗\)\.\\displaystyle=\\mathsf\{Conf\}^\{\\ast\}\(\\mathsf\{Hard\}^\{\\ast\},\\mathsf\{Soft\}^\{\\ast\}\_\{0\}\)\\cup\\mathsf\{Conf\}^\{\\ast\}\(\\mathsf\{Soft\}^\{\\ast\}\_\{0\}\)\.Permissions trigger hard conflicts without overriding hard obligations, while soft conflicts are warnings; hence𝖯​\(κ\)\\mathsf\{P\}\(\\kappa\)and𝖭𝖱​\(κ\)\\mathsf\{NR\}\(\\kappa\)are consistent by default\.

Let

𝖵𝗂𝗈𝗅∗\\displaystyle\\mathsf\{Viol\}^\{\\ast\}=\{n∣𝗌𝗍𝖺𝗍𝖾​\(𝗏𝗂𝗈𝗅𝖺𝗍𝖾𝖽,n\)∈Σ∗\},\\displaystyle=\\\{n\\mid\\mathsf\{state\}\(\\mathsf\{violated\},n\)\\in\\Sigma^\{\\ast\}\\\},𝖴𝗇𝗄∗\\displaystyle\\mathsf\{Unk\}^\{\\ast\}=\{n∣𝗌𝗍𝖺𝗍𝖾\(𝗉𝖾𝗇𝖽𝗂𝗇𝗀,n\)∈Σ∗\\displaystyle=\\\{n\\mid\\mathsf\{state\}\(\\mathsf\{pending\},n\)\\in\\Sigma^\{\\ast\}or𝗌𝗍𝖺𝗍𝖾\(𝗎𝗇𝗄𝗇𝗈𝗐𝗇,n\)∈Σ∗\}\.\\displaystyle\\hskip 28\.00006pt\\text\{or \}\\mathsf\{state\}\(\\mathsf\{unknown\},n\)\\in\\Sigma^\{\\ast\}\\\}\.The aggregate status is

𝗌𝗍𝖺𝗍𝗎𝗌∗=\{𝖼𝗈𝗇𝖿𝗅𝗂𝖼𝗍𝖾𝖽𝖧𝖢∗≠∅,𝗏𝗂𝗈𝗅𝖺𝗍𝖾𝖽𝖵𝗂𝗈𝗅∗≠∅,𝗎𝗇𝗄𝗇𝗈𝗐𝗇𝖴𝗇𝗄∗≠∅,𝖼𝗈𝗆𝗉𝗅𝗂𝖺𝗇𝗍otherwise\.\\mathsf\{status\}^\{\\ast\}=\\begin\{cases\}\\mathsf\{conflicted\}&\\mathsf\{HC\}^\{\\ast\}\\neq\\emptyset,\\\\ \\mathsf\{violated\}&\\mathsf\{Viol\}^\{\\ast\}\\neq\\emptyset,\\\\ \\mathsf\{unknown\}&\\mathsf\{Unk\}^\{\\ast\}\\neq\\emptyset,\\\\ \\mathsf\{compliant\}&\\text\{otherwise\}\.\\end\{cases\}Finally,

𝖮𝗎𝗍ℬη​\(I\)=⟨Σ∗,G∗,𝖧𝖢∗,𝖲𝖢∗,𝗌𝗍𝖺𝗍𝗎𝗌∗⟩\.\\mathsf\{Out\}^\{\\eta\}\_\{\\mathcal\{B\}\}\(I\)=\\langle\\Sigma^\{\\ast\},G^\{\\ast\},\\mathsf\{HC\}^\{\\ast\},\\mathsf\{SC\}^\{\\ast\},\\mathsf\{status\}^\{\\ast\}\\rangle\.

###### Proposition 5\(Exactness of declared conflicts\)\.

The set𝖧𝖢∗\\mathsf\{HC\}^\{\\ast\}contains exactly the hard\-hard and hard\-permission pairs whose signed targets are incompatible under⟂O\\perp\_\{O\}\. The set𝖲𝖢∗\\mathsf\{SC\}^\{\\ast\}contains exactly the hard\-soft and soft\-soft pairs, after soft absorption, whose signed targets are incompatible under⟂O\\perp\_\{O\}\.

###### Proof sketch\.

This follows directly from the definitions of𝖢𝗈𝗇𝖿∗\\mathsf\{Conf\}^\{\\ast\},𝖧𝖢∗\\mathsf\{HC\}^\{\\ast\},𝖲𝖢∗\\mathsf\{SC\}^\{\\ast\}, and𝖲𝗈𝖿𝗍0∗\\mathsf\{Soft\}^\{\\ast\}\_\{0\}\. ∎

### Examples

Representative ADAS\-style examples illustrate MONIR\-core modelling patterns\.

###### Example 1\(Basic operational patterns\)\.

Consider three stylized clauses:

> C1\. If automated lane keeping is active and the driver does not respond to a takeover request, the system shall initiate a minimal\-risk maneuver\. C2\. If C1 applies and at least two risk conditions hold, C3 shall apply\. C3\. When C3 applies, the system shall satisfy the required safe\-action condition\.

Cross\-references are expanded into factual triggers:

c1\\displaystyle c\_\{1\}:𝖺𝗅𝗄𝗌​\_​𝖺𝖼𝗍𝗂𝗏𝖾∧𝗍𝗈𝗋​\_​𝗍𝗂𝗆𝖾𝗈𝗎𝗍↝𝖼𝟣​\_​𝖺𝗉𝗉𝗅𝗂𝖾𝗌,\\displaystyle:\\ \\mathsf\{alks\\\_active\}\\wedge\\mathsf\{tor\\\_timeout\}\\leadsto\\mathsf\{c1\\\_applies\},c2\\displaystyle c\_\{2\}:𝖼𝟣​\_​𝖺𝗉𝗉𝗅𝗂𝖾𝗌∧𝖼𝗈𝗎𝗇𝗍\[2,3\]​\(𝗌𝗁𝗈𝗎𝗅𝖽𝖾𝗋​\_​𝗎𝗇𝖺𝗏𝖺𝗂𝗅𝖺𝖻𝗅𝖾,𝗈𝖻𝗌𝗍𝖺𝖼𝗅𝖾​\_​𝖺𝗁𝖾𝖺𝖽,𝗅𝗈𝗐​\_​𝗏𝗂𝗌𝗂𝖻𝗂𝗅𝗂𝗍𝗒\)\\displaystyle:\\ \\mathsf\{c1\\\_applies\}\\wedge\\mathsf\{count\}\_\{\[2,3\]\}\\left\(\\begin\{array\}\[\]\{l\}\\mathsf\{shoulder\\\_unavailable\},\\\\ \\mathsf\{obstacle\\\_ahead\},\\\\ \\mathsf\{low\\\_visibility\}\\end\{array\}\\right\)↝𝖼𝟥​\_​𝖺𝗉𝗉𝗅𝗂𝖾𝗌\.\\displaystyle\\qquad\\leadsto\\mathsf\{c3\\\_applies\}\.The corresponding normative rules are

n1\\displaystyle n\_\{1\}:𝖼𝟣​\_​𝖺𝗉𝗉𝗅𝗂𝖾𝗌⇒𝖮​\(𝗆𝗋𝗆\),\\displaystyle:\\ \\mathsf\{c1\\\_applies\}\\Rightarrow\\mathsf\{O\}\(\\mathsf\{mrm\}\),n2\\displaystyle n\_\{2\}:𝖼𝟥​\_​𝖺𝗉𝗉𝗅𝗂𝖾𝗌⇒𝖮​\(𝖼𝗈𝗎𝗇𝗍\[2,3\]​\(𝗋𝖾𝖽𝗎𝖼𝖾​\_​𝗌𝗉𝖾𝖾𝖽,𝗌𝗍𝖺𝗒​\_​𝗂𝗇​\_​𝗅𝖺𝗇𝖾,𝖺𝗎𝖽𝗂𝗈​\_​𝗐𝖺𝗋𝗇\)\)\.\\displaystyle:\\ \\mathsf\{c3\\\_applies\}\\Rightarrow\\mathsf\{O\}\\left\(\\mathsf\{count\}\_\{\[2,3\]\}\\left\(\\begin\{array\}\[\]\{l\}\\mathsf\{reduce\\\_speed\},\\\\ \\mathsf\{stay\\\_in\\\_lane\},\\\\ \\mathsf\{audio\\\_warn\}\\end\{array\}\\right\)\\right\)\.Exemption disables an otherwise applicable rule:

n3:𝖾𝗆𝖾𝗋𝗀𝖾𝗇𝖼𝗒​\_​𝖾𝗏𝖺𝗌𝗂𝗈𝗇⇒𝖾𝗑𝖾𝗆𝗉𝗍​\(n2\)\.n\_\{3\}:\\ \\mathsf\{emergency\\\_evasion\}\\Rightarrow\\mathsf\{exempt\}\(n\_\{2\}\)\.This is admissible only ifn3n\_\{3\}is evaluated beforen2n\_\{2\}\. Normative conflict is detected during aggregation:

n4:𝗈𝖻𝗌𝗍𝖺𝖼𝗅𝖾​\_​𝖺𝗁𝖾𝖺𝖽⇒𝖮​\(¬𝗌𝗍𝖺𝗒​\_​𝗂𝗇​\_​𝗅𝖺𝗇𝖾\)\.n\_\{4\}:\\ \\mathsf\{obstacle\\\_ahead\}\\Rightarrow\\mathsf\{O\}\(\\neg\\mathsf\{stay\\\_in\\\_lane\}\)\.If an active rule also requires𝗌𝗍𝖺𝗒​\_​𝗂𝗇​\_​𝗅𝖺𝗇𝖾\\mathsf\{stay\\\_in\\\_lane\}, the signed targets\+𝗌𝗍𝖺𝗒​\_​𝗂𝗇​\_​𝗅𝖺𝗇𝖾\+\\mathsf\{stay\\\_in\\\_lane\}and\+\(¬𝗌𝗍𝖺𝗒​\_​𝗂𝗇​\_​𝗅𝖺𝗇𝖾\)\+\(\\neg\\mathsf\{stay\\\_in\\\_lane\}\)conflict under⟂O\\perp\_\{O\}\. This affects𝖧𝖢∗\\mathsf\{HC\}^\{\\ast\}and𝗌𝗍𝖺𝗍𝗎𝗌∗\\mathsf\{status\}^\{\\ast\}\. Unknown evidence is represented by rule states:

n5:𝗁𝖾𝖺𝗏𝗒​\_​𝗋𝖺𝗂𝗇⇒𝖮​\(𝗋𝖾𝖽𝗎𝖼𝖾​\_​𝗌𝗉𝖾𝖾𝖽\)\.n\_\{5\}:\\ \\mathsf\{heavy\\\_rain\}\\Rightarrow\\mathsf\{O\}\(\\mathsf\{reduce\\\_speed\}\)\.If𝗁𝖾𝖺𝗏𝗒​\_​𝗋𝖺𝗂𝗇\\mathsf\{heavy\\\_rain\}is true and𝗋𝖾𝖽𝗎𝖼𝖾​\_​𝗌𝗉𝖾𝖾𝖽\\mathsf\{reduce\\\_speed\}is unknown inI∗I^\{\\ast\}, then𝗌𝗍𝖺𝗍𝖾​\(𝗎𝗇𝗄𝗇𝗈𝗐𝗇,n5\)∈Σ∗\\mathsf\{state\}\(\\mathsf\{unknown\},n\_\{5\}\)\\in\\Sigma^\{\\ast\}\. If𝗁𝖾𝖺𝗏𝗒​\_​𝗋𝖺𝗂𝗇\\mathsf\{heavy\\\_rain\}is unknown, then𝗌𝗍𝖺𝗍𝖾​\(𝗉𝖾𝗇𝖽𝗂𝗇𝗀,n5\)∈Σ∗\\mathsf\{state\}\(\\mathsf\{pending\},n\_\{5\}\)\\in\\Sigma^\{\\ast\}andn5n\_\{5\}generates no active output\.

###### Example 2\(Violations and staged reparations\)\.

Consider a stylized collision\-response requirement:

> If a forward collision risk is detected, the system shall issue a collision warning\. If the warning is not issued, the system shall initiate emergency braking\. If emergency braking is not initiated, the system shall request a minimal\-risk maneuver and record the event\.

It is represented by

n6\\displaystyle n\_\{6\}:𝖼𝗈𝗅𝗅𝗂𝗌𝗂𝗈𝗇​\_​𝗋𝗂𝗌𝗄⇒𝖮​\(𝖼𝗈𝗅𝗅𝗂𝗌𝗂𝗈𝗇​\_​𝗐𝖺𝗋𝗇\),\\displaystyle:\\ \\mathsf\{collision\\\_risk\}\\Rightarrow\\mathsf\{O\}\(\\mathsf\{collision\\\_warn\}\),n7\\displaystyle n\_\{7\}:𝗌𝗍𝖺𝗍𝖾​\(𝗏𝗂𝗈𝗅𝖺𝗍𝖾𝖽,n6\)⇒𝖮​\(𝖾𝗆𝖾𝗋𝗀𝖾𝗇𝖼𝗒​\_​𝖻𝗋𝖺𝗄𝖾\),\\displaystyle:\\ \\mathsf\{state\}\(\\mathsf\{violated\},n\_\{6\}\)\\Rightarrow\\mathsf\{O\}\(\\mathsf\{emergency\\\_brake\}\),n8\\displaystyle n\_\{8\}:𝗌𝗍𝖺𝗍𝖾​\(𝗏𝗂𝗈𝗅𝖺𝗍𝖾𝖽,n7\)⇒𝖮​\(𝗆𝗋𝗆​\_​𝗅𝗈𝗀\)\.\\displaystyle:\\ \\mathsf\{state\}\(\\mathsf\{violated\},n\_\{7\}\)\\Rightarrow\\mathsf\{O\}\(\\mathsf\{mrm\\\_log\}\)\.Rulen6n\_\{6\}is the primary obligation, andn7,n8n\_\{7\},n\_\{8\}are reparational obligations\. Admissibility requiresλN​\(n6\)<λN​\(n7\)<λN​\(n8\)\\lambda\_\{N\}\(n\_\{6\}\)<\\lambda\_\{N\}\(n\_\{7\}\)<\\lambda\_\{N\}\(n\_\{8\}\)\. The local reparation outcome is read fromΣ∗\\Sigma^\{\\ast\}\. If𝖼𝗈𝗅𝗅𝗂𝗌𝗂𝗈𝗇​\_​𝗐𝖺𝗋𝗇\\mathsf\{collision\\\_warn\}is false and𝖾𝗆𝖾𝗋𝗀𝖾𝗇𝖼𝗒​\_​𝖻𝗋𝖺𝗄𝖾\\mathsf\{emergency\\\_brake\}is true, then

𝗌𝗍𝖺𝗍𝖾​\(𝗏𝗂𝗈𝗅𝖺𝗍𝖾𝖽,n6\)\\displaystyle\\mathsf\{state\}\(\\mathsf\{violated\},n\_\{6\}\)∈Σ∗,\\displaystyle\\in\\Sigma^\{\\ast\},𝗌𝗍𝖺𝗍𝖾​\(𝖿𝗎𝗅𝖿𝗂𝗅𝗅𝖾𝖽,n7\)\\displaystyle\\mathsf\{state\}\(\\mathsf\{fulfilled\},n\_\{7\}\)∈Σ∗\.\\displaystyle\\in\\Sigma^\{\\ast\}\.The aggregate status remains𝗏𝗂𝗈𝗅𝖺𝗍𝖾𝖽\\mathsf\{violated\}, while the trace records a fulfilled reparation\. If𝖾𝗆𝖾𝗋𝗀𝖾𝗇𝖼𝗒​\_​𝖻𝗋𝖺𝗄𝖾\\mathsf\{emergency\\\_brake\}is false, then𝗌𝗍𝖺𝗍𝖾​\(𝗏𝗂𝗈𝗅𝖺𝗍𝖾𝖽,n7\)∈Σ∗\\mathsf\{state\}\(\\mathsf\{violated\},n\_\{7\}\)\\in\\Sigma^\{\\ast\}, son8n\_\{8\}may be activated\.

###### Example 3\(Patterns excluded by admissibility\)\.

Admissibility excludes modelling patterns with unstable operational meaning\.

First, evidential feedback lets derived facts change their own support:

b1\\displaystyle b\_\{1\}:𝖼𝗈𝗎𝗇𝗍\[1,1\]​\(𝗋𝖺𝖽𝖺𝗋​\_​𝗈𝖻𝗌,𝖼𝖺𝗆𝖾𝗋𝖺​\_​𝗈𝖻𝗌\)↝𝖽𝖾𝗀𝗋𝖺𝖽𝖾𝖽,\\displaystyle:\\ \\mathsf\{count\}\_\{\[1,1\]\}\\left\(\\begin\{array\}\[\]\{l\}\\mathsf\{radar\\\_obs\},\\\\ \\mathsf\{camera\\\_obs\}\\end\{array\}\\right\)\\leadsto\\mathsf\{degraded\},b2\\displaystyle b\_\{2\}:𝖽𝖾𝗀𝗋𝖺𝖽𝖾𝖽↝𝖼𝖺𝗆𝖾𝗋𝖺​\_​𝗈𝖻𝗌\.\\displaystyle:\\ \\mathsf\{degraded\}\\leadsto\\mathsf\{camera\\\_obs\}\.This creates a cyclic factual dependency and violates F\-Stratification\.

Second, cyclic state dependence lets two rules require each other’s state:

b3\\displaystyle b\_\{3\}:𝗌𝗍𝖺𝗍𝖾​\(𝗏𝗂𝗈𝗅𝖺𝗍𝖾𝖽,b4\)⇒𝖮​\(𝗍𝖺𝗄𝖾𝗈𝗏𝖾𝗋​\_​𝗋𝖾𝗊\),\\displaystyle:\\ \\mathsf\{state\}\(\\mathsf\{violated\},b\_\{4\}\)\\Rightarrow\\mathsf\{O\}\(\\mathsf\{takeover\\\_req\}\),b4\\displaystyle b\_\{4\}:𝗌𝗍𝖺𝗍𝖾​\(𝗏𝗂𝗈𝗅𝖺𝗍𝖾𝖽,b3\)⇒𝖮​\(𝗆𝗂𝗇𝗂𝗆𝖺𝗅​\_​𝗋𝗂𝗌𝗄\)\.\\displaystyle:\\ \\mathsf\{state\}\(\\mathsf\{violated\},b\_\{3\}\)\\Rightarrow\\mathsf\{O\}\(\\mathsf\{minimal\\\_risk\}\)\.No ordering satisfies both dependencies, so N\-Stratification fails\.

Third, retroactive exemption exempts a rule only after its state is fixed:

b5\\displaystyle b\_\{5\}:𝗈𝖻𝗌𝗍𝖺𝖼𝗅𝖾​\_​𝖽𝖾𝗍𝖾𝖼𝗍𝖾𝖽⇒𝖥​\(𝖺𝖼𝖼𝖾𝗅𝖾𝗋𝖺𝗍𝖾\),\\displaystyle:\\ \\mathsf\{obstacle\\\_detected\}\\Rightarrow\\mathsf\{F\}\(\\mathsf\{accelerate\}\),b6\\displaystyle b\_\{6\}:𝗌𝗍𝖺𝗍𝖾​\(𝗏𝗂𝗈𝗅𝖺𝗍𝖾𝖽,b5\)⇒𝖾𝗑𝖾𝗆𝗉𝗍​\(b5\)\.\\displaystyle:\\ \\mathsf\{state\}\(\\mathsf\{violated\},b\_\{5\}\)\\Rightarrow\\mathsf\{exempt\}\(b\_\{5\}\)\.Here N\-Stratification requiresλN​\(b5\)<λN​\(b6\)\\lambda\_\{N\}\(b\_\{5\}\)<\\lambda\_\{N\}\(b\_\{6\}\), while E\-Admissibility requiresλN​\(b6\)<λN​\(b5\)\\lambda\_\{N\}\(b\_\{6\}\)<\\lambda\_\{N\}\(b\_\{5\}\)\. Hence the pattern is inadmissible\.

### Basic Properties and Expressive Boundary

###### Definition 8\(Dependency graphs\)\.

For a well\-formed rule baseℬ=⟨RP,RN⟩\\mathcal\{B\}=\\langle R\_\{P\},R\_\{N\}\\rangle, define the factual dependency graphGP=\(RP,EP\)G\_\{P\}=\(R\_\{P\},E\_\{P\}\)and the normative dependency graphGN=\(RN,EN\)G\_\{N\}=\(R\_\{N\},E\_\{N\}\)\. For proposition rules,

\(ρ′,ρ\)∈EP​iff​𝖠𝗍​\(𝗁𝖾𝖺𝖽​\(ρ′\)\)∩𝖠𝗍​\(𝖻𝗈𝖽𝗒​\(ρ\)\)≠∅\.\(\\rho^\{\\prime\},\\rho\)\\in E\_\{P\}\\text\{ iff \}\\mathsf\{At\}\(\\mathsf\{head\}\(\\rho^\{\\prime\}\)\)\\cap\\mathsf\{At\}\(\\mathsf\{body\}\(\\rho\)\)\\neq\\emptyset\.For normative rules,ENE\_\{N\}contains the following two kinds of edges:

\(r′,r\)∈EN\\displaystyle\(r^\{\\prime\},r\)\\in E\_\{N\}iff​𝗌𝗍𝖺𝗍𝖾​\(s,𝗂𝖽​\(r′\)\)∈𝖲𝗍​\(𝖻𝗈𝖽𝗒​\(r\)\)for some​s∈𝒮,\\displaystyle\\text\{ iff \}\\begin\{array\}\[t\]\{l\}\\mathsf\{state\}\(s,\\mathsf\{id\}\(r^\{\\prime\}\)\)\\in\\mathsf\{St\}\(\\mathsf\{body\}\(r\)\)\\\\ \\text\{for some \}s\\in\\mathcal\{S\},\\end\{array\}\(r,r′\)∈EN\\displaystyle\(r,r^\{\\prime\}\)\\in E\_\{N\}iff​𝗈𝗎𝗍​\(r\)=𝖾𝗑𝖾𝗆𝗉𝗍​\(𝗂𝖽​\(r′\)\)\.\\displaystyle\\text\{ iff \}\\mathsf\{out\}\(r\)=\\mathsf\{exempt\}\(\\mathsf\{id\}\(r^\{\\prime\}\)\)\.Thus,GPG\_\{P\}records factual dependencies, whileGNG\_\{N\}records state reads and non\-retroactive exemptions\.

###### Proposition 6\(Admissibility as acyclicity\)\.

A well\-formed MONIR\-core rule base is admissible iff bothGPG\_\{P\}andGNG\_\{N\}are acyclic\.

###### Proof sketch\.

If admissibility holds, each edge inGPG\_\{P\}orGNG\_\{N\}strictly increases the corresponding witnessing rank\. A directed cycle would therefore imply a strict inequality from a rank to itself, impossible\.

Conversely, if both graphs are acyclic, take any topological ranking ofGPG\_\{P\}asλP\\lambda\_\{P\}and any topological ranking ofGNG\_\{N\}asλN\\lambda\_\{N\}\. The edges ofGPG\_\{P\}enforce F\-Stratification, while the two edge types ofGNG\_\{N\}enforce N\-Stratification and E\-Admissibility\. ∎

###### Proposition 7\(Independence of witnessing stratifications\)\.

Letη\\etabe a regular three\-valued evaluator, letℬ\\mathcal\{B\}be admissible, and letIIbe an input interpretation\. Any two witnessing factual stratifications yield the same factual outcome: either both reject due to a complementary factual conflict, or both produce the same closureI∗I^\{\\ast\}\. In the latter case, any two witnessing normative stratifications yield the same normative result⟨Σ∗,G∗⟩\\langle\\Sigma^\{\\ast\},G^\{\\ast\}\\rangleand the same aggregate output𝖮𝗎𝗍ℬη​\(I\)\\mathsf\{Out\}^\{\\eta\}\_\{\\mathcal\{B\}\}\(I\)\.

###### Proof sketch\.

By Proposition[6](https://arxiv.org/html/2606.04619#Thmtheorem6),GPG\_\{P\}andGNG\_\{N\}are acyclic\. Witnessing stratifications are topological rankings of these graphs\. Different rankings only reorder independent rules, which do not read each other’s derived facts, states, or exemptions\. Thus the factual outcome and⟨Σ∗,G∗⟩\\langle\\Sigma^\{\\ast\},G^\{\\ast\}\\rangleare unchanged\. Since aggregation is deterministic inΣ∗\\Sigma^\{\\ast\},G∗G^\{\\ast\}, and⟂O\\perp\_\{O\},𝖮𝗎𝗍ℬη​\(I\)\\mathsf\{Out\}^\{\\eta\}\_\{\\mathcal\{B\}\}\(I\)is unchanged\. ∎

###### Theorem 8\(Well\-definedness of staged evaluation\)\.

Letη\\etabe a regular three\-valued evaluator, letℬ=⟨RP,RN⟩\\mathcal\{B\}=\\langle R\_\{P\},R\_\{N\}\\ranglebe an admissible MONIR\-core rule base, and letIIbe an input interpretation\. Then exactly one of the following holds:

1. 1\.factual closure is undefined because a complementary factual conflict is derived;
2. 2\.factual closureI∗I^\{\\ast\}is defined, normative evaluation yields a unique pair⟨Σ∗,G∗⟩\\langle\\Sigma^\{\\ast\},G^\{\\ast\}\\rangle, and aggregation yields a unique output𝖮𝗎𝗍ℬη​\(I\)\\mathsf\{Out\}^\{\\eta\}\_\{\\mathcal\{B\}\}\(I\)with a unique status𝗌𝗍𝖺𝗍𝗎𝗌∗\\mathsf\{status\}^\{\\ast\}\.

The second outcome is independent of the witnessing stratifications\.

###### Proof\.

Fix witnessing stratificationsλP\\lambda\_\{P\}andλN\\lambda\_\{N\}\. SinceRPR\_\{P\}andRNR\_\{N\}are finite, both staged evaluations have finitely many occupied strata\. In the factual stage, induction over strata gives a unique sequenceI≤kI\_\{\\leq k\}: each stratum is determined by the previous interpretation, and Lemma[1](https://arxiv.org/html/2606.04619#Thmtheorem1)ensures stable body values\. Hence factual evaluation either uniquely rejects a complementary conflict or yields a unique closureI∗I^\{\\ast\}\.

IfI∗I^\{\\ast\}is defined, induction over normative strata gives a unique sequence of rule states and generated outputs\. State\-dependent bodies are stable by Lemma[4](https://arxiv.org/html/2606.04619#Thmtheorem4), and E\-Admissibility makes exemptions available before their target rules are evaluated\. Hence⟨Σ∗,G∗⟩\\langle\\Sigma^\{\\ast\},G^\{\\ast\}\\rangleis unique\.

Aggregation is deterministic inΣ∗\\Sigma^\{\\ast\},G∗G^\{\\ast\}, and⟂O\\perp\_\{O\}\. Therefore𝖮𝗎𝗍ℬη​\(I\)\\mathsf\{Out\}^\{\\eta\}\_\{\\mathcal\{B\}\}\(I\)and𝗌𝗍𝖺𝗍𝗎𝗌∗\\mathsf\{status\}^\{\\ast\}are unique\. Independence from the witnessing stratifications follows from Proposition[7](https://arxiv.org/html/2606.04619#Thmtheorem7)\. ∎

###### Proposition 9\(Two\-valued conservativity\)\.

Letη\\etabe a regular three\-valued evaluator and letIIbe complete over𝒫\\mathcal\{P\}, that is,I\+∪I−=𝒫I^\{\+\}\\cup I^\{\-\}=\\mathcal\{P\}\. If factual closure is defined, then every factual formula and every normative condition evaluated during staged evaluation has a bivalent value\. Hence no rule receives state𝗉𝖾𝗇𝖽𝗂𝗇𝗀\\mathsf\{pending\}, and no active𝖮\\mathsf\{O\}\- or𝖥\\mathsf\{F\}\-rule receives state𝗎𝗇𝗄𝗇𝗈𝗐𝗇\\mathsf\{unknown\}\.

###### Proof sketch\.

Completeness ofIImakes every factual atom bivalent\. Sinceη\\etais classically conservative on bivalent valuations, factual formulas evaluate classically\. By N\-Stratification, every state atom read by a normative rule refers only to a lower\-stratum rule whose state has already been fixed, so state tests are also bivalent\. Therefore normative bodies are bivalent\. If an𝖮\\mathsf\{O\}\- or𝖥\\mathsf\{F\}\-rule is active, its target is a factual formula over a bivalent factual closure, so its target is bivalent as well\. ∎

The dependency graphs also give an incremental admissibility check\. After inserting a well\-formed ruleqq, it is enough to addqqand its incident edges to the corresponding graph and test acyclicity\. With indexes for rule identifiers and occurring atoms, the edge update costsO​\(\|q\|\+dq\)O\(\|q\|\+d\_\{q\}\), wheredqd\_\{q\}is the number of new incident edges; a full acyclicity test costsO​\(\|V\|\+\|E\|\)O\(\|V\|\+\|E\|\)\.

Cardinality expressions are evaluated throughη\\etaafter translation\. For𝖼𝗈𝗎𝗇𝗍\[l,u\]​\(x1,…,xm\)\\mathsf\{count\}\_\{\[l,u\]\}\(x\_\{1\},\\ldots,x\_\{m\}\), the explicit𝖠𝗍𝖫𝖾𝖺𝗌𝗍\\mathsf\{AtLeast\}translation has size

O​\(\(ml\)​l\+\(mu\+1\)​\(u\+1\)\),O\\left\(\\binom\{m\}\{l\}l\+\\binom\{m\}\{u\+1\}\(u\+1\)\\right\),with constant\-size cases for𝖠𝗍𝖫𝖾𝖺𝗌𝗍0\\mathsf\{AtLeast\}\_\{0\}and𝖠𝗍𝖫𝖾𝖺𝗌𝗍k\\mathsf\{AtLeast\}\_\{k\}whenk\>mk\>m\. The reason is that𝖠𝗍𝖫𝖾𝖺𝗌𝗍k\\mathsf\{AtLeast\}\_\{k\}contains\(mk\)\\binom\{m\}\{k\}conjunctions of lengthkk\. Thus, explicit expansion is polynomial only for bounded arity, unless a direct polynomial\-time cardinality evaluator equivalent to the translation is used\.

###### Corollary 10\(Polynomial fragments\)\.

If all cardinality arities are bounded by a constant, and if signed\-target construction, target comparison, and membership in⟂O\\perp\_\{O\}are polynomial\-time computable, then MONIR\-core evaluation is polynomial in the source rule\-base size\. The same holds for any polynomial\-time direct cardinality evaluator that agrees with the explicit translation\.

###### Proof sketch\.

Bounded arity makes the translated formulas polynomial in size\. The factual, normative, and aggregation stages then inspect polynomially many rules, states, outputs, signed targets, and conflict pairs, each using polynomial\-time tests\. ∎

MONIR\-core is deterministic for a fixed input interpretation, but it is not monotonic under input refinement\. Upper\-bounded cardinality conditions and explicit negative evidence may turn a previously true condition into false\. Thus, MONIR\-core defines snapshot evaluation; updates are handled by re\-evaluation or by the MONIR\-ASP layer\.

## MONIR\-ASP: From Core Semantics to ASP Solving

MONIR\-ASP provides an executable realization of MONIR\. An admissible MONIR rule base is reified as ASP facts and evaluated by a fixed kernel program\. Numeric and temporal reasoning are treated as engineering extensions: they may supply additional proposition values and maintain reasoning snapshots for efficiency, but they do not modify the normative kernel\.

### Semantic Realization of MONIR\-core

This subsection specifies the core MONIR\-ASP compilation and proves its behavioral faithfulness to MONIR\-core\. The compilation follows the fact\-based style of ASP metaprogramming, where source\-level objects are represented as facts and interpreted by a fixed kernel\(Kaminskiet al\.[2023](https://arxiv.org/html/2606.04619#bib.bib27)\)\. In our setting, the reified objects are MONIR rules, formula nodes, strata, outputs, evidence snapshots, and declared incompatibilities\.

A core evidence snapshot over𝒫\\mathcal\{P\}is a consistent partial inputS=⟨S\+,S−⟩S=\\langle S^\{\+\},S^\{\-\}\\rangle, whereS\+,S−⊆𝒫S^\{\+\},S^\{\-\}\\subseteq\\mathcal\{P\}andS\+∩S−=∅S^\{\+\}\\cap S^\{\-\}=\\emptyset\. It is read as the MONIR\-core inputIS=⟨S\+,S−⟩I\_\{S\}=\\langle S^\{\+\},S^\{\-\}\\rangle; atoms outsideS\+∪S−S^\{\+\}\\cup S^\{\-\}are unknown\.

A core MONIR\-ASP instance isℐ𝖼𝗈𝗋𝖾=⟨ℬ,S,η⟩\\mathcal\{I\}\_\{\\mathsf\{core\}\}=\\langle\\mathcal\{B\},S,\\eta\\rangle, whereℬ\\mathcal\{B\}is an admissible MONIR\-core rule base,SSis a core evidence snapshot, andη\\etais the selected three\-valued evaluator\. The compiler produces

Π​\(ℐ𝖼𝗈𝗋𝖾\)=Fℬ∪FS∪Π𝗏𝖺𝗅∪Π𝖾𝗏𝖺𝗅∪Π𝗇𝗈𝗋𝗆∪Π𝖺𝗀𝗀,\\Pi\(\\mathcal\{I\}\_\{\\mathsf\{core\}\}\)=F\_\{\\mathcal\{B\}\}\\cup F\_\{S\}\\cup\\Pi\_\{\\mathsf\{val\}\}\\cup\\Pi\_\{\\mathsf\{eval\}\}\\cup\\Pi\_\{\\mathsf\{norm\}\}\\cup\\Pi\_\{\\mathsf\{agg\}\},whereFℬF\_\{\\mathcal\{B\}\}andFSF\_\{S\}contain the reified rule base and snapshot\. The kernel components compute proposition values, formula values, normative states, conflicts, and status\.

Formulae are reified as identifiers rather than inlined into ASP rule bodies\. The kernel exposes formula evaluation through𝖾𝗏𝖺𝗅​\(f,v\)\\mathsf\{eval\}\(f,v\), whereffis a formula identifier andv∈\{𝐭,𝐟,𝐮\}v\\in\\\{\\mathbf\{t\},\\mathbf\{f\},\\mathbf\{u\}\\\}\. Its implementation realizes the selected evaluatorη\\etaover the reified formula structure\.

###### Example 4\(Source\-level reification\)\.

Consider the MONIR fragmentρ1:p∧¬q↝a\\rho\_\{1\}:p\\wedge\\neg q\\leadsto a,n1:a⇒𝖮​\(m\)n\_\{1\}:a\\Rightarrow\\mathsf\{O\}\(m\), andn2:𝗌𝗍𝖺𝗍𝖾​\(𝗏𝗂𝗈𝗅𝖺𝗍𝖾𝖽,n1\)⇒𝖾𝗑𝖾𝗆𝗉𝗍​\(n3\)n\_\{2\}:\\mathsf\{state\}\(\\mathsf\{violated\},n\_\{1\}\)\\Rightarrow\\mathsf\{exempt\}\(n\_\{3\}\), wheren3n\_\{3\}is a later rule with output𝖥​\(m\)\\mathsf\{F\}\(m\)\. A possible source\-level reification is:

```
prule(rho1). plev(rho1,0).
body(rho1,f_rho1). head(rho1,pos(a)).
conj(f_rho1).
arg(f_rho1,1,f_p). arg(f_rho1,2,f_not_q).
lit(f_p,p). neg_lit(f_not_q,q).

norm(n1). nlev(n1,0).
body(n1,f_a). out(n1,o(f_m)).
lit(f_a,a). lit(f_m,m).

norm(n2). nlev(n2,1).
body(n2,f_v). out(n2,exempt(n3)).
state_test(f_v,violated,n1).

norm(n3). nlev(n3,2).
body(n3,f_a). out(n3,f(f_m)).

incompat(pos(f_m),neg(f_m)).
```

The predicates𝗉𝗋𝗎𝗅𝖾/1\\mathsf\{prule\}/1and𝗇𝗈𝗋𝗆/1\\mathsf\{norm\}/1classify rules, while𝗉𝗅𝖾𝗏/2\\mathsf\{plev\}/2and𝗇𝗅𝖾𝗏/2\\mathsf\{nlev\}/2record the levels maintained during admissible rule\-base construction\. The kernel uses these levels to enforce the derivation order\.

The predicate𝖻𝗈𝖽𝗒/2\\mathsf\{body\}/2maps each rule to a body formula; proposition rules additionally use𝗁𝖾𝖺𝖽/2\\mathsf\{head\}/2for derived literals, and normative rules use𝗈𝗎𝗍/2\\mathsf\{out\}/2for modalized outputs\. Formula nodes are reified by facts such as𝖼𝗈𝗇𝗃/1\\mathsf\{conj\}/1,𝖺𝗋𝗀/3\\mathsf\{arg\}/3,𝗅𝗂𝗍/2\\mathsf\{lit\}/2,𝗇𝖾𝗀​\_​𝗅𝗂𝗍/2\\mathsf\{neg\\\_lit\}/2, and𝗌𝗍𝖺𝗍𝖾​\_​𝗍𝖾𝗌𝗍/3\\mathsf\{state\\\_test\}/3\. In the example,𝗌𝗍𝖺𝗍𝖾​\_​𝗍𝖾𝗌𝗍​\(fv,𝗏𝗂𝗈𝗅𝖺𝗍𝖾𝖽,n1\)\\mathsf\{state\\\_test\}\(f\_\{v\},\\mathsf\{violated\},n\_\{1\}\)is admissible becausen1n\_\{1\}is belown2n\_\{2\}in the normative strata\.

Finally,𝗂𝗇𝖼𝗈𝗆𝗉𝖺𝗍/2\\mathsf\{incompat\}/2reifies aggregation\-level incompatibility, e\.g\.,𝗂𝗇𝖼𝗈𝗆𝗉𝖺𝗍​\(𝗉𝗈𝗌​\(fm\),𝗇𝖾𝗀​\(fm\)\)\\mathsf\{incompat\}\(\\mathsf\{pos\}\(f\_\{m\}\),\\mathsf\{neg\}\(f\_\{m\}\)\)states that requiringmmconflicts with requiring avoidance ofmm\.

Listings[1](https://arxiv.org/html/2606.04619#listing1)show the minimal kernel rules used in the faithfulness argument\. It treat𝗏𝖺𝗅/2\\mathsf\{val\}/2as the interface for final proposition values and omit the full factual\-closure encoding and the internal implementation of𝖾𝗏𝖺𝗅/2\\mathsf\{eval\}/2; these components must agree with the MONIR\-core factual closure and the selected evaluatorη\\eta\. The predicate𝗅𝗍/2\\mathsf\{lt\}/2is a fixed strict order used only to avoid duplicate conflict pairs\. Cardinality may be implemented by direct counting instead of materializing the explicit𝖠𝗍𝖫𝖾𝖺𝗌𝗍\\mathsf\{AtLeast\}expansion, provided that it agrees with the cardinality semantics forη\\eta\.

Listing 1Core normative\-aggregation k kernel\.bval\(N,V\):\-norm\(N\),body\(N,F\),eval\(F,V\)\.

exb\(N\):\-gen\(M,exempt\(N\)\),nlev\(M,J\),nlev\(N,K\),J<K\.

gen\(N,O\):\-norm\(N\),bval\(N,t\),out\(N,O\),notexb\(N\)\.

st\(out,N\):\-norm\(N\),bval\(N,f\)\.

st\(pending,N\):\-norm\(N\),bval\(N,u\)\.

st\(inactive,N\):\-norm\(N\),bval\(N,t\),exb\(N\)\.

st\(fulfilled,N\):\-gen\(N,o\(F\)\),eval\(F,t\)\.

st\(violated,N\):\-gen\(N,o\(F\)\),eval\(F,f\)\.

st\(unknown,N\):\-gen\(N,o\(F\)\),eval\(F,u\)\.

st\(fulfilled,N\):\-gen\(N,f\(F\)\),eval\(F,f\)\.

st\(violated,N\):\-gen\(N,f\(F\)\),eval\(F,t\)\.

st\(unknown,N\):\-gen\(N,f\(F\)\),eval\(F,u\)\.

st\(effective,N\):\-gen\(N,p\(F\)\)\.

st\(effective,N\):\-gen\(N,r\(F\)\)\.

st\(effective,N\):\-gen\(N,nr\(F\)\)\.

st\(effective,N\):\-gen\(N,exempt\(M\)\)\.

h\(N,pos\(F\)\):\-gen\(N,o\(F\)\)\.h\(N,neg\(F\)\):\-gen\(N,f\(F\)\)\.

s\(N,pos\(F\)\):\-gen\(N,r\(F\)\)\.s\(N,neg\(F\)\):\-gen\(N,nr\(F\)\)\.

p\(N,pos\(F\)\):\-gen\(N,p\(F\)\)\.

hard\(T\):\-h\(\_,T\)\.

s0\(N,T\):\-s\(N,T\),nothard\(T\)\.

hc\(N,M\):\-h\(N,T1\),h\(M,T2\),lt\(N,M\),incompat\(T1,T2\)\.

hc\(N,M\):\-h\(N,T1\),p\(M,T2\),N\!=M,incompat\(T1,T2\)\.

sc\(N,M\):\-h\(N,T1\),s0\(M,T2\),N\!=M,incompat\(T1,T2\)\.

sc\(N,M\):\-s0\(N,T1\),s0\(M,T2\),lt\(N,M\),incompat\(T1,T2\)\.

status\(conflicted\):\-hc\(N,M\)\.

status\(violated\):\-notstatus\(conflicted\),st\(violated,N\)\.

status\(unknown\):\-notstatus\(conflicted\),notstatus\(violated\),st\(pending,N\)\.

status\(unknown\):\-notstatus\(conflicted\),notstatus\(violated\),st\(unknown,N\)\.

status\(compliant\):\-notstatus\(conflicted\),notstatus\(violated\),notstatus\(unknown\)\.

###### Proposition 12\(Stratified core program\)\.

Letℬ\\mathcal\{B\}be an admissible MONIR\-core rule base with maintained factual and normative levels\. Assume thatΠ𝗏𝖺𝗅\\Pi\_\{\\mathsf\{val\}\}follows the factual levels, that the reified formula graph is acyclic, and thatΠ𝖾𝗏𝖺𝗅\\Pi\_\{\\mathsf\{eval\}\}is a deterministic stratified implementation of the selected evaluatorη\\eta\. If the factual closure ofISI\_\{S\}is defined, then the ground core programΠ​\(ℐ𝖼𝗈𝗋𝖾\)\\Pi\(\\mathcal\{I\}\_\{\\mathsf\{core\}\}\)is stratified and has a unique stable model\.

###### Proof sketch\.

By construction, the program layers follow𝗉𝗅𝖾𝗏/2\\mathsf\{plev\}/2, the acyclic formula graph,𝗇𝗅𝖾𝗏/2\\mathsf\{nlev\}/2, and then the aggregation stage\. Admissibility rules out factual cycles, cyclic state reads, and retroactive exemptions, so all dependencies are well founded and every negative dependency points to a lower layer\. Thus the ground program is stratified\. With defined factual closure and deterministic kernel components, the stable model is unique\. ∎

Faithfulness is stated on the observable predicates𝗌𝗍/2\\mathsf\{st\}/2,𝗀𝖾𝗇/2\\mathsf\{gen\}/2,𝗁𝖼/2\\mathsf\{hc\}/2,𝗌𝖼/2\\mathsf\{sc\}/2, and𝗌𝗍𝖺𝗍𝗎𝗌/1\\mathsf\{status\}/1\. For the stable modelXXofΠ​\(ℐ𝖼𝗈𝗋𝖾\)\\Pi\(\\mathcal\{I\}\_\{\\mathsf\{core\}\}\),π𝖼𝗈𝗋𝖾​\(X\)\\pi\_\{\\mathsf\{core\}\}\(X\)denotes the projection that maps𝗌𝗍​\(s,n\)\\mathsf\{st\}\(s,n\)to𝗌𝗍𝖺𝗍𝖾​\(s,n\)\\mathsf\{state\}\(s,n\),𝗀𝖾𝗇​\(n,ω\)\\mathsf\{gen\}\(n,\\omega\)to\(n,ω\)\(n,\\omega\),𝗁𝖼​\(n,m\)\\mathsf\{hc\}\(n,m\)and𝗌𝖼​\(n,m\)\\mathsf\{sc\}\(n,m\)to unordered conflict pairs, and𝗌𝗍𝖺𝗍𝗎𝗌​\(s\)\\mathsf\{status\}\(s\)to the aggregate status\. Auxiliary atoms are ignored\.

The compilation is behaviorally faithful iff, whenever𝖮𝗎𝗍ℬη​\(IS\)\\mathsf\{Out\}^\{\\eta\}\_\{\\mathcal\{B\}\}\(I\_\{S\}\)is defined,

π𝖼𝗈𝗋𝖾​\(X\)=𝖮𝗎𝗍ℬη​\(IS\)\.\\pi\_\{\\mathsf\{core\}\}\(X\)=\\mathsf\{Out\}^\{\\eta\}\_\{\\mathcal\{B\}\}\(I\_\{S\}\)\.
###### Theorem 13\(Faithfulness of the core compilation\)\.

Letℬ\\mathcal\{B\}be an admissible MONIR\-core rule base,SSa core evidence snapshot, andISI\_\{S\}the input determined bySS\. Suppose thatΠ𝗏𝖺𝗅\\Pi\_\{\\mathsf\{val\}\}agrees with the MONIR\-core factual closure, thatΠ𝖾𝗏𝖺𝗅\\Pi\_\{\\mathsf\{eval\}\}implements the selected evaluatorη\\eta, and that any direct cardinality implementation agrees with the MONIR\-core cardinality semantics forη\\eta\. If𝖮𝗎𝗍ℬη​\(IS\)\\mathsf\{Out\}^\{\\eta\}\_\{\\mathcal\{B\}\}\(I\_\{S\}\)is defined, thenΠ​\(ℐ𝖼𝗈𝗋𝖾\)\\Pi\(\\mathcal\{I\}\_\{\\mathsf\{core\}\}\)is behaviorally faithful to MONIR\-core\.

###### Proof sketch\.

By construction, the value and evaluator components reproduce the factual closure and formula values of MONIR\-core\. Admissibility makes state reads and exemptions well founded, so the normative kernel derives the same generated outputs and rule states\. The aggregation kernel uses the same target construction, incompatibility relation, and status priority\. Hence the observable projection equals𝖮𝗎𝗍ℬη​\(IS\)\\mathsf\{Out\}^\{\\eta\}\_\{\\mathcal\{B\}\}\(I\_\{S\}\)\. ∎

If the factual closure ofISI\_\{S\}is undefined, MONIR\-core has no ordinary output\. An implementation may still report diagnostic atoms, but such atoms are outside𝖮𝖻𝗌𝖼𝗈𝗋𝖾\\mathsf\{Obs\}\_\{\\mathsf\{core\}\}\.

The maintained levels induce a dependency DAG over kernel components\. For each factual or normative level and each kernel stage, ground rules with disjoint exported atoms can be grouped into modules\. A module reads only reification facts, exported atoms of predecessor modules, or fixed lower\-level results\.

###### Proposition 14\(Level\-wise modularity\)\.

For an admissible rule base, the ground core program admits a modular decomposition ordered by factual levels, normative levels, and aggregation stages\. Modules with disjoint exported signatures and no cyclic positive dependency are joinable; their compatible stable models compose to the stable model of their union\.

###### Proof sketch\.

By construction, module dependencies follow the maintained levels and the fixed kernel\-stage order\. Admissibility rules out factual cycles, cyclic state reads, and retroactive exemptions\. Hence there is no cross\-module positive recursion, and exported signatures are disjoint by the chosen decomposition\. The claim follows from the ASP module theorem\. ∎

A runtime snapshot stores the exported atoms of evaluated modules\. After an evidence updateΔ​S\\Delta S, let𝒜\\mathcal\{A\}be the least set of affected modules containing all value modules whose inputs may change, and closed under the module\-dependency DAG\. Modules in𝒜\\mathcal\{A\}are recomputed in topological order; all other exported atoms are reused\.

###### Proposition 15\(Soundness of delta\-local reuse\)\.

Assume that the rule base, maintained levels, evaluator, and kernel are fixed\. For an evidence updateΔ​S\\Delta S, recomputing exactly the affected modules𝒜\\mathcal\{A\}and reusing all other cached exported atoms yields the same observable core projection as full recomputation on the updated snapshot\.

###### Proof sketch\.

Proceed by induction over the module\-dependency DAG\. Unaffected source modules have unchanged inputs and therefore unchanged deterministic outputs\. For any later module, either some predecessor may change, in which case the module is in𝒜\\mathcal\{A\}and is recomputed, or all predecessor exports are unchanged, in which case its output is unchanged\. Thus every module export matches full recomputation, and so does the observable projection\. ∎

## References

- G\. Brewka, T\. Eiter, and M\. Truszczyński \(2011\)Answer set programming at a glance\.Communications of the ACM54\(12\),pp\. 92–103\.Cited by:[Introduction](https://arxiv.org/html/2606.04619#Sx1.p2.1)\.
- T\. B\. Brown, B\. Mann, N\. Ryder, M\. Subbiah, J\. D\. Kaplan, D\. Amodei,et al\.\(2020\)Language models are few\-shot learners\.InAdvances in Neural Information Processing Systems,Vol\.33,pp\. 1877–1901\.Cited by:[LLM\-Assisted Extraction](https://arxiv.org/html/2606.04619#Sx2.SSx2.p1.4)\.
- M\. Gebser, R\. Kaminski, B\. Kaufmann, and T\. Schaub \(2019\)Multi\-shot ASP solving with clingo\.Theory and Practice of Logic Programming19\(1\),pp\. 27–82\.External Links:[Document](https://dx.doi.org/10.1017/S1471068418000054)Cited by:[Introduction](https://arxiv.org/html/2606.04619#Sx1.p4.1)\.
- M\. Gelfond and V\. Lifschitz \(1988\)The stable model semantics for logic programming\.InProceedings of the Fifth International Conference and Symposium on Logic Programming,pp\. 1070–1080\.Cited by:[Answer Set Programming](https://arxiv.org/html/2606.04619#Sx2.SSx1.p2.3)\.
- G\. Governatori and A\. Rotolo \(2006\)Logic of violations: a gentzen system for reasoning with contrary\-to\-duty obligations\.Australasian Journal of Logic4,pp\. 193–215\.External Links:[Document](https://dx.doi.org/10.26686/ajl.v4i0.1780)Cited by:[Remark 11](https://arxiv.org/html/2606.04619#Thmtheorem11.p1.3)\.
- R\. Kaminski, J\. Romero, T\. Schaub, and P\. Wanko \(2023\)How to build your own asp\-based system?\!\.Theory and Practice of Logic Programming23\(1\),pp\. 299–361\.External Links:[Document](https://dx.doi.org/10.1017/S1471068421000508)Cited by:[Semantic Realization of MONIR\-core](https://arxiv.org/html/2606.04619#Sx4.SSx1.p1.1)\.
- S\. C\. Kleene \(1952\)Introduction to metamathematics\.North\-Holland,Amsterdam\.Cited by:[Operational Semantics](https://arxiv.org/html/2606.04619#Sx3.SSx2.p3.3)\.
- D\. Makinson and L\. van der Torre \(2000\)Input/output logics\.Journal of Philosophical Logic29\(4\),pp\. 383–408\.External Links:[Document](https://dx.doi.org/10.1023/A%3A1004748624537)Cited by:[Introduction](https://arxiv.org/html/2606.04619#Sx1.p3.1),[Remark 11](https://arxiv.org/html/2606.04619#Thmtheorem11.p1.3)\.
- P\. McNamara and F\. Van De Putte \(2006\)Deontic logic\.InThe Stanford Encyclopedia of Philosophy,E\. N\. Zalta \(Ed\.\),Cited by:[Remark 11](https://arxiv.org/html/2606.04619#Thmtheorem11.p1.3)\.
- E\. Oikarinen and T\. Janhunen \(2006\)Modular equivalence for normal logic programs\.InProceedings of the Ninth European Conference on Logics in Artificial Intelligence,Lecture Notes in Computer Science, Vol\.4160,pp\. 412–416\.External Links:[Document](https://dx.doi.org/10.1007/11853886%5F34)Cited by:[Introduction](https://arxiv.org/html/2606.04619#Sx1.p4.1),[Answer Set Programming](https://arxiv.org/html/2606.04619#Sx2.SSx1.p3.11)\.
- L\. Robaldo, S\. Batsakis, R\. Calegari, F\. Calimeri, M\. Fujita, G\. Governatori, M\. C\. Morelli, F\. Pisano, K\. Satoh, I\. Tachmazidis, and J\. Zangari \(2024\)Compliance checking on first\-order knowledge with conflicting and compensatory norms: a comparison among currently available technologies\.Artificial Intelligence and Law32,pp\. 505–552\.External Links:[Document](https://dx.doi.org/10.1007/s10506-023-09360-z)Cited by:[Introduction](https://arxiv.org/html/2606.04619#Sx1.p2.1)\.