Augustine Mochoeneng: Lexicographic Closure

Contribution

I built the workbench end to end and used it to test the alignment theorem with Lexicographic Closure.

Workbench: an executable version of the ECCRS-to-KLM translation, written in C.
Lexicographic Closure: entailment over the translated knowledge base.
Verification: MSW against LC on every instance of three benchmark rule sets.
Violation study: rule sets that break each assumption on purpose, to see how the agreement fails.

Approach

The idea behind Lexicographic Closure

Rational Closure answers a query by throwing away whole ranks of statements until the query makes sense. That is often too blunt: penguins lose "birds have wings" just because it sits in the same rank as "birds fly". Lexicographic Closure keeps as much as it can and discards only what actually clashes.

How it is computed

BaseRank

Rank statements from general to specific, exactly as Rational Closure does.

$$\mathcal{E}_{i+1} = \{ \alpha \dent \beta \in \mathcal{E}_i : \overrightarrow{\mathcal{E}_i} \models \neg\alpha \}$$

SubsetRank

Split each rank by how many of its statements are kept, so keeping more beats keeping fewer.

$$\mathcal{D}_{i,j} = \bigvee_{X \subseteq \mathcal{B}_i,\ |X| = j} \ \bigwedge_{x \in X} \overrightarrow{x}$$

Query

Run the usual removal loop on the finer ranking: drop one layer at a time until the antecedent is consistent, then check the consequent.

$$\mathcal{K} \models_{LC} F \dent m \iff \overrightarrow{\mathcal{R}_{\geq k}} \models F \rightarrow m$$

Implementation

Assumption validator: checks sanity, strict exception closure and no total override before anything runs, and halts with a report if one fails.
MSW side: computes $\mathcal{A}(F)$ and $\mathcal{M}(F)$ and writes an explanation trace for every instance.
Translator: maps each rule to one typical statement, linear in the size of the rule set.
Reasoner: every consistency check goes to a SAT solver (PicoSAT, bundled with the code), and instances are answered in parallel with OpenMP.
Agreement check: compares the two verdicts per instance and sorts each into agree, abstain, disagree or conflict.

Results

When the assumptions hold

Rule set	Instances	MSW = LC
Bank	11,303	100%
Breast Cancer	175	100%
Mushroom	2,031	100%
Total	13,509	100%

When an assumption is broken

Assumption broken	Agree	Abstain	Conflict
Exception closure	13,395	114	0
Sanity	12,019	0	1,490
No total override	13,374	0	135

Exception closure broken: one or both sides abstain instead of guessing.
Sanity or total override broken: LC entails both labels, and the instance is flagged as a conflict.
Total override: the 135 conflicts are exactly the instances where ECCRS itself changed its answer.

Agreement is perfect when the theorem's assumptions hold, and when they break the check fails safely: never a confident wrong label.