Lightweight axiom pinpointing via replicated driver and customized SAT-solving

查看全文 作　　者：Dantong [1,2]OUYANG;Mengting [1]LIAO;Yuxin [1,2]YE

机构地区：[1]College of Computer Science and Technology,Jilin University,Changchun 130012,China;[2]Key Laboratory of Symbolic Computation and Knowledge Engineering(Jilin University),Ministry of Education,Changchun 130012,China

出　　处：《Frontiers of Computer Science》索引2023年第17卷第2期,共13页

基　　金：supported by the National Natural Science Foundation of China(NSFC)(Grant Nos.42050103,62076108,and U19A2061). 摘　　要：In description logic,axiom pinpointing is used to explore defects in ontologies and identify hidden justifications for a logical consequence.In recent years,SAT-based axiom pinpointing techniques,which rely on the enumeration of minimal unsatisfiable subsets(MUSes)of pinpointing formulas,have gained increasing attention.Compared with traditional Tableau-based reasoning approaches,SAT-based techniques are more competitive when computing justifications for consequences in large-scale lightweight description logic ontologies.In this article,we propose a novel enumeration justification algorithm,working with a replicated driver.The replicated driver discovers new justifications from the explored justifications through cheap literals resolution,which avoids frequent calls of SAT solver.Moreover,when the use of SAT solver is inevitable,we adjust the strategies and heuristic parameters of the built-in SAT solver of axiom pinpointing algorithm.The adjusted SAT solver is able to improve the checking efficiency of unexplored sub-formulas.Our proposed method is implemented as a tool named RDMinA.The experimental results show that RDMinA outperforms the existing axiom pinpointing tools on practical biomedical ontologies such as Gene,Galen,NCI and Snomed-CT. 关键词：axiom pinpointing description logic SAT solver

相关文献

参考文献（37）
引证文献（1）
耦合文献（0）

参考文献(37)

引证文献(1)

互联网出版许可证新出网证(渝)字10号全国400电话 - 免长途话费

Lightweight axiom pinpointing via replicated driver and customized SAT-solving

参考文献(37)

引证文献(1)

用户提示