Computing General First-Order Parallel and Prioritized Circumscription


  • Hai Wan Sun Yat-sen University
  • Zhanhao Xiao Sun Yat-sen University
  • Zhenfeng Yuan Sun Yat-sen University
  • Heng Zhang University of Western Sydney
  • Yan Zhang University of Western Sydney



Parallel and Prioritized Circumscription, Stable Model Semantics, Solver


This paper focuses on computing general first-order parallel and prioritized circumscription with varying constants. We propose linear translations from general first-order circumscription to first-order theories under stable model semantics over arbitrary structures, including Tr_v for parallel circumscription and Tr^s_v for conjunction of parallel circumscriptions (further for prioritized circumscription). To improve the efficiency, we give an optimization \Gamma_{\exists} to reduce logic programs in size when eliminating existential quantifiers during the translations. Based on these results, a general first-order circumscription solver, named cfo2lp, is developed by calling answer set programming (ASP) solvers. Using circuit diagnosis problem and extended stable marriage problem as benchmarks, we compare cfo2lp with a propositional circumscription solver circ2dlp and an ASP solver with complex optimization metasp on efficiency. Experimental results demonstrate that for problems represented by first-order circumscription naturally and intuitively, cfo2lp can compute all solutions over finite structures. We also apply our approach to description logics with circumscription and repairs in inconsistent databases, which can be handled effectively.




How to Cite

Wan, H., Xiao, Z., Yuan, Z., Zhang, H., & Zhang, Y. (2014). Computing General First-Order Parallel and Prioritized Circumscription. Proceedings of the AAAI Conference on Artificial Intelligence, 28(1).



AAAI Technical Track: Knowledge Representation and Reasoning