TY - GEN
T1 - On loop formulas with variables
AU - Lee, Joohyung
AU - Meng, Yunsong
N1 - Copyright:
Copyright 2021 Elsevier B.V., All rights reserved.
PY - 2008
Y1 - 2008
N2 - Recently Ferraris, Lee and Lifschitz proposed a new definition of stable models that does not refer to grounding, which applies to the syntax of arbitrary first-order sentences. We show its relation to the idea of loop formulas with variables by Chen, Lin, Wang and Zhang, and generalize their loop formulas to disjunctive programs and to arbitrary first-order sentences. We also extend the syntax of logic programs to allow explicit quantifiers, and define its semantics as a subclass of the new language of stable models by Ferraris et al. Such programs inherit from the general language the ability to handle nonmonotonic reasoning under the stable model semantics even in the absence of the unique name and the domain closure assumptions, while yielding more succinct loop formulas than the general language due to the restricted syntax. We also show certain syntactic conditions under which query answering for an extended program can be reduced to entailment checking in first-order logic, providing a way to apply first-order theorem provers to reasoning about non-Herbrand stable models.
AB - Recently Ferraris, Lee and Lifschitz proposed a new definition of stable models that does not refer to grounding, which applies to the syntax of arbitrary first-order sentences. We show its relation to the idea of loop formulas with variables by Chen, Lin, Wang and Zhang, and generalize their loop formulas to disjunctive programs and to arbitrary first-order sentences. We also extend the syntax of logic programs to allow explicit quantifiers, and define its semantics as a subclass of the new language of stable models by Ferraris et al. Such programs inherit from the general language the ability to handle nonmonotonic reasoning under the stable model semantics even in the absence of the unique name and the domain closure assumptions, while yielding more succinct loop formulas than the general language due to the restricted syntax. We also show certain syntactic conditions under which query answering for an extended program can be reduced to entailment checking in first-order logic, providing a way to apply first-order theorem provers to reasoning about non-Herbrand stable models.
UR - http://www.scopus.com/inward/record.url?scp=69949141510&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=69949141510&partnerID=8YFLogxK
M3 - Conference contribution
AN - SCOPUS:69949141510
SN - 9781577353843
T3 - Proceedings of the International Conference on Knowledge Representation and Reasoning
SP - 444
EP - 453
BT - Principles of Knowledge Representation and Reasoning
PB - Institute of Electrical and Electronics Engineers Inc.
T2 - 11th International Conference on Principles of Knowledge Representation and Reasoning, KR 2008
Y2 - 16 September 2008 through 19 September 2008
ER -