NMR Workshop 2025 Conference Paper
Toward Defeasible Reasoning Using Knowledge Compilation Techniques
- Luke Slater
- Thomas Andreas Meyer
- Jesse Heyninck
We explore the use of ordered binary decision diagrams (OBDDs) and multi-terminal binary decision diagrams (MTBDDs) for compiling and executing defeasible reasoning, focusing on System Z, also known as rational closure. We introduce an OBDD-based algorithm for System Z inference that parallels traditional SAT-based approaches. Additionally, we investigate the use of MTBDDs for encoding ordinal conditional functions (OCFs), providing a more general and unified knowledge compilation framework for defeasible reasoning tasks involving ranking functions. While our primary focus is on System Z, the proposed techniques are applicable to other forms of defeasible reasoning and conditional logic more broadly. Experimental results demonstrate that OBDDs can significantly accelerate inference. However, our evaluation is limited to synthetically generated belief bases, and further research is needed to validate benefits in real-world scenarios. Overall, our findings suggest that binary decision diagrams offer a promising alternative to SAT-based methods for defeasible reasoning, and warrant further investigation.