When: Thursday, November 17, 2022, 3pm (CET).

Where: Zoom online.

Topic: Knowledge Compilation Meets Logical Separability.

Speaker: Junming Qiu, a MSc student at Jinan University, China.

Abstract

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 work, 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 logical separability-based languages into the knowledge compilation map.

The talk is based on the paper: [AAAI-2022] Knowledge Compilation Meets Logical Separability.

Short Bio

Junming Qiu is a MSc student at Jinan University, China. His main research interests lie in automated reasoning, including knowledge compilation and belief change.

Material