Antony Baker: Rational Closure

Contribution

I built the EDRS workbench which translates to System W belief bases and runs the Inference using InfOCF System W implementation.

Workbench: an executable version of the ECCRS-to-KLM translation, written in Python.
System W: entailment over the translated knowledge base.
Verification: MSW against System W on every instance of three benchmark rule sets.

Approach

The idea behind System W

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 \}$$

SubsetInclusion

H contains either the non-falsifying formula or the falsifying formula for every conditional in the belief base.

$$\mathcal{H} = \bigcup_{i \in \{j+1,...,k\}} nf(\Delta_{nf}^i) \cup \overline{nf\Delta_{f}^i}$$

Query

Run the query check each set of conditionals layer by layer until we have checked all falsifying or non-falsifying conditionals. The query is entailed if it is not falsified by any of the sets of conditionals.

$$\mathcal{K} \models_{SW} 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 (z3, bundled with the code).
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 = SW
Bank	11,303	100%
Breast Cancer	175	100%
Mushroom	2,031	100%
Total	13,509	100%