Translating First-Order Theories into Logic Programs

Abstract

This paper focuses on computing first-order theories under either stable model semantics or circumscription. A reduction from first-order theories to logic programs under stable model semantics over finite structures is proposed, and an embedding of circumscription into stable model semantics is also given. Having such reduction and embedding, reasoning problems represented by first-order theories under these two semantics can then be handled by using existing answer set solvers. The effectiveness of this approach in computing hard problems beyond NP is demonstrated by some experiments.

Cite

Text

Zhang et al. "Translating First-Order Theories into Logic Programs." International Joint Conference on Artificial Intelligence, 2011. doi:10.5591/978-1-57735-516-8/IJCAI11-192

Markdown

[Zhang et al. "Translating First-Order Theories into Logic Programs." International Joint Conference on Artificial Intelligence, 2011.](https://mlanthology.org/ijcai/2011/zhang2011ijcai-translating/) doi:10.5591/978-1-57735-516-8/IJCAI11-192

BibTeX

@inproceedings{zhang2011ijcai-translating,
  title     = {{Translating First-Order Theories into Logic Programs}},
  author    = {Zhang, Heng and Zhang, Yan and Ying, Mingsheng and Zhou, Yi},
  booktitle = {International Joint Conference on Artificial Intelligence},
  year      = {2011},
  pages     = {1126-1131},
  doi       = {10.5591/978-1-57735-516-8/IJCAI11-192},
  url       = {https://mlanthology.org/ijcai/2011/zhang2011ijcai-translating/}
}