Knowledge Compilation Meets Logical Separability


  • Junming Qiu Jinan University Guangdong Institute of Smart Education
  • Wenqing Li Jinan University Guangdong Institute of Smart Education
  • Zhanhao Xiao Sun Yat-sen University
  • Quanlong Guan Jinan University Guangdong Institute of Smart Education
  • Liangda Fang Jinan University Pazhou Lab Guangxi Key Laboratory of Trusted Software
  • Zhao-Rong Lai Jinan University Guangdong Institute of Smart Education
  • Qian Dong Jinan University



Knowledge Representation And Reasoning (KRR)


Knowledge compilation is an alternative solution to address demanding reasoning tasks with high complexity via converting knowledge bases into a suitable target language. Interestingly, the notion of logical separability, proposed by Levesque, offers a general explanation for the tractability of clausal entailment for two remarkable languages: decomposable negation normal form and prime implicates. It is interesting to explore what role logical separability on earth plays in problem tractability. In this paper, we apply the notion of logical separability in three reasoning problems within the context of propositional logic: satisfiability check (CO), clausal entailment check (CE) and model counting (CT), contributing to three corresponding polytime procedures. We provide three logical separability based properties: CO- logical separability, CE-logical separability and CT-logical separability. We then identify three novel normal forms: CO-LSNNF, CE-LSNNF and CT-LSNNF based on the above properties. Besides, we show that every normal form is the necessary and sufficient condition under which the corresponding procedure is correct. We finally integrate the above four normal forms into the knowledge compilation map.




How to Cite

Qiu, J., Li, W., Xiao, Z., Guan, Q., Fang, L., Lai, Z.-R., & Dong, Q. (2022). Knowledge Compilation Meets Logical Separability. Proceedings of the AAAI Conference on Artificial Intelligence, 36(5), 5851-5860.



AAAI Technical Track on Knowledge Representation and Reasoning