Thumbnail
Access Restriction
Subscribed

Author Kolaitis, Phokion G. ♦ Papadimitriou, Christos H.
Source ACM Digital Library
Content type Text
Publisher Association for Computing Machinery (ACM)
File Format PDF
Copyright Year ©1990
Language English
Subject Domain (in DDC) Computer science, information & general works ♦ Data processing & computer science
Subject Keyword Circumscription ♦ Horn ♦ Model checking ♦ NP-completeness ♦ First-order logic ♦ Nonmonotonic reasoning ♦ Undecidability
Abstract The effects of circumscribing first-order formulas are explored from a computational standpoint. First, extending work of V. Lifschitz, it is Shown that the circumscription of any existential first-order formula is equivalent to a first-order formula. After this, it is established that a set of universal Horn clauses has a first-order circumscription if and only if it is bounded (when considered as a logic program); thus it is undecidable to tell whether such formulas have first-order circumscription. Finally, it is shown that there arefirst-order formulas whode circumscription has a coNP-complete model-checking problem.
ISSN 00045411
Age Range 18 to 22 years ♦ above 22 year
Educational Use Research
Education Level UG and PG
Learning Resource Type Article
Publisher Date 1990-01-03
Publisher Place New York
e-ISSN 1557735X
Journal Journal of the ACM (JACM)
Volume Number 37
Issue Number 1
Page Count 14
Starting Page 1
Ending Page 14


Open content in new tab

   Open content in new tab
Source: ACM Digital Library