Daniel Schlesinger: Rational Closure

Contribution

I developed the EDRS workbench end to end and used it to evaluate the alignment theorem, which states that Rational Closure (RC) and Most Specific Wins (MSW) yield identical predictions on every instance of a rule set satisfying three structural conditions. I also designed an optimised RC procedure that reduces the satisfiability calls required to evaluate the largest rule set from 98,304 to 102.

Workbench: a Python command-line application that parses an ECCRS rule set, validates it, translates it into a KLM knowledge base, evaluates RC and MSW, and presents both explanation traces side by side. It has no runtime dependencies.
Rational Closure: BaseRank and entailment checking, implemented from first principles, including the SAT solver.
Optimisation: a 964-fold reduction in solver calls on Bank Marketing, with identical results.
Verification: a comparison of RC and MSW on three benchmark rule sets, together with a scholarship rule set that deliberately violates the theorem's assumptions.

Approach

The idea behind Rational Closure

Rational Closure orders the statements of a knowledge base by their degree of exceptionality. A query is answered by discarding the most general ranks until its premise is consistent with the remaining statements, and then testing whether the conclusion follows. The alignment theorem is formulated with respect to RC, and both Lexicographic Closure and System W extend its ranking.

How it is computed

BaseRank

Statements whose premise is inconsistent with the remaining knowledge base are removed iteratively. Each removed layer is assigned the next rank, and any statement never removed receives rank $\infty$.

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

Base rank of a query

The lowest rank at which the premise is consistent with the statements at that rank and above.

$$br_{\mathcal{K}}(\alpha) = \min \{ i : \overrightarrow{\mathcal{R}_{\geq i}} \not\models \neg\alpha \}$$

Entailment

Each instance $F$ is queried twice, once for $m$ and once for $\neg m$.

$$\mathcal{K} \models_{RC} F \dent m \iff br_{\mathcal{K}}(F) \lt br_{\mathcal{K}}(F \land \neg m)$$

Optimisation

Verifying the theorem requires querying RC on every complete feature pattern. Bank Marketing has 16,384 of these, and each requires several calls to the SAT solver. The central observation is that MSW and RC depend on a pattern solely through the set of rules applicable to it. Since many patterns share the same applicable rules, the workbench partitions them into equivalence classes by a direct lookup that requires no solver calls. It evaluates each class once and weights the result by the size of the class. The procedure is exact, and it is verified against the ungrouped computation on every pattern. In addition, a binary search over the ranks determines each base rank in $O(\log k)$ solver calls.

Satisfiability calls for the full pattern-space check
Rule set	Patterns	Before	Grouped	Speed-up
Breast Cancer	64	400	64	6×
Mushroom	1,024	6,144	66	93×
Bank Marketing	16,384	98,304	102	964×

On Bank Marketing, execution time is reduced from 3.24 seconds to 0.10 seconds.

Implementation

Assumption validator: checks sanity, strict global exception closure and no total override. It reports every violation and returns a non-zero exit status, while completing the run so that the effect of a violation remains observable.
MSW: computed directly from the rule set and independent of the translation, providing an independent check on RC.
Translator: maps each rule to exactly one defeasible conditional over a fresh class atom $m$.
Reasoner: BaseRank and entailment built on a DPLL SAT solver implemented from first principles in Python.
Explanation traces: the ECCRS override chain presented alongside the RC rank comparison. Both identify the same deciding rule.
Testing: validation against published worked examples, differential testing against an independent brute-force oracle over 312 random knowledge bases and 3,120 queries, and a pattern-by-pattern comparison of grouped and ungrouped results.

Results

When the assumptions hold

Rule set	Holdout instances	All instances	Complete patterns	MSW = RC
Breast Cancer	175	699	64	100%
Mushroom	2,031	8,124	1,024	100%
Bank Marketing	11,303	45,211	16,384	100%
Total	13,509	54,034	17,472	100%

No disagreements or abstentions occurred in any population.
On the 771 holdout instances in which a rule is overridden by a more specific rule, RC agrees with MSW in every case.
An independent implementation supplied with the datasets reproduces the workbench's MSW labels, applicable rules and maximal rules on all 13,509 holdout instances.

When the assumptions are violated

On a small scholarship rule set that violates the theorem's assumptions, RC and MSW diverge on a single pattern out of 32, which is precisely the pattern identified by the validator. They agree on all remaining patterns.