Some computational aspects of circumscription

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.

REFERENCES

• 1: Alfred V. Aho , Jeffrey D. Ullman, Universality of data retrieval languages, Proceedings of the 6th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.110-119, January 29-31, 1979, San Antonio, Texas [doi>10.1145/567752.567763]
• 2: BARWISE, K.J. Admissible Sets and Structures: An Approach to Definability Theory. Springer- Verlag, New York, 1975.
• 3: BARWISE, K. J., AND MOSCHOVAKIS, Y.N. Uniform inductive definability. J. Symb. Logic 43 (1978), 521-534.
• 4: Genevieve Bossu , Pierre Siegel, Saturation, nonmonotonic reasoning and the closed-world assumption, Artificial Intelligence, v.25 n.1, p.13-63, Jan. 1985 [doi>10.1016/0004-3702(85)90040-2]
• 5: CHANDRA, A. K., AND HAREL, D. Structure and complexity of relational queries. J. Comput. Syst. Sci. 25 (1982), 99-128.
• 6: CHANG, C. C., AND KEISLER, H.J. Model Theory. North-Holland, Amsterdam, The Netherlands, 1973.
• 7: Stavros Cosmadakis , Haim Gaifman , Paris Kanellakis , Moshe Vardi, Decidable optimization problems for database logic programs, Proceedings of the twentieth annual ACM symposium on Theory of computing, p.477-490, May 02-04, 1988, Chicago, Illinois, United States [doi>10.1145/62212.62259]
• 8: DAVIS, M. The mathematics of non-monotonic reasoning. Artif. Int. 13 (1980), 73-80.
• 9: J Doyle, Circumscription and implicit definability, Journal of Automated Reasoning, v.1 n.4, p.391-405, 1985
• 10: ETHERINGTON, D., MERCER, R., AND REITER, R. On the adequacy of predicate circumscription for closed-world reasoning. Computat. Intelligence 1 (1985), 1 l- 15.
• 11: FAGIN, R. Generalized first-order spectra and polynomial-time recognizable sets. In Complexity of Computations, R. Karp, ed. Proceedings of the SIAM-AMS, vol. 7. American Mathematical Society, Providence, R.I., 1974, pp. 43-74.
• 12: GAIFMAN, H., MAIRSON, H., SAGIV, Y., AND VARDI, M.Y. Undecidable optimization problems for database logic programs. In Proceedings of the 2nd IEEE Symposium on Logic in Computer Science. IEEE, New York, 1987, pp. 106-115.
• 13: GELFOND, M., AND LIFSCHITZ, V. Compiling circumscriptive theories into logic programs. In Proceedings of the 7th National Conference on Artificial Intelligence (AAAI 88) (Aug.), vol. 2. Morgan-Kaufmann, San Mateo, Calif., 1988, pp. 455-459.
• 14: GELFOND, M., PRZYMUSINSKA, H., AND PRZYMUSINSKI, T. Minimal model semantics vs. negation as failure: A comparison of semantics. In Proceedings of the ACM SIGART Symposium on Methodologies for Intelligence Systems (Torino, Italy). ACM, New York, 1988.
• 15: Michael R. Genesereth , Nils J. Nilsson, Logical foundations of artificial intelligence, Morgan Kaufmann Publishers Inc., San Francisco, CA, 1987
• 16: IOANNIDES, Y.E. A time bound on the materialization of some recursively defined views. In Proceedings of the 1 l th International Conference on Very Large Data Bases. Morgan-Kaufrnann, San Mateo, Calif., 1985, pp. 219-226.
• 17: T. Krishnaprasad, On the computability of circumscription, Information Processing Letters, v.27 n.5, p.237-243, April 28, 1988 [doi>10.1016/0020-0190(88)90085-3]
• 18: KUEKER, D.W. Decidability results for universal sentences true on minimal models, preprint. University of Maryland, College Park, Md., 1987.
• 19: LIFSCHITZ, V. Computing circumscription. In Proceedings of the 9th International Joint Conference on Artificial Intelligence. 1985, pp. 121-127.
• 20: Vladimir Lifschitz, On the satisfiability of circumscription, Artificial Intelligence, v.28 n.1, p.17-27, Feb. 1986 [doi>10.1016/0004-3702(86)90028-7]
• 21: V. Lifschitz, Pointwise circumscription, Readings in nonmonotonic reasoning, Morgan Kaufmann Publishers Inc., San Francisco, CA, 1987
• 22: David Maier , Jeffrey D. Ullman , Moshe Y. Vardi, On the foundations of the universal relation model, ACM Transactions on Database Systems (TODS), v.9 n.2, p.283-308, June 1984 [doi>10.1145/329.318580]
• 23: MCCARTHY, J. CircumscriptionmA form of non-monotonic reasoning. Artif. Int. 13 (1980), 27-39.
• 24: John McCarthy, Applications of circumscription to formalizing common-sense knowledge, Artificial Intelligence, v.28 n.1, p.89-116, Feb. 1986 [doi>10.1016/0004-3702(86)90032-9]
• 25: Yiannis N Moschovakis, Elementary induction on abstract structures (Studies in logic and the foundations of mathematics), American Elsevier Pub. Co, 1974
• 26: Jeff Naughton, Data independent recursion in deductive databases, Proceedings of the fifth ACM SIGACT-SIGMOD symposium on Principles of database systems, p.267-279, March 24-26, 1986, Cambridge, Massachusetts, United States [doi>10.1145/6012.15420]
• 27: J. F. Naughton , Y. Sagiv, A decidable class of bounded recursions, Proceedings of the sixth ACM SIGACT-SIGMOD-SIGART symposium on Principles of database systems, p.227-236, March 23-25, 1987, San Diego, California, United States [doi>10.1145/28659.28684]
• 28: Christos H. Papadimitriou , Kenneth Steiglitz, Combinatorial optimization: algorithms and complexity, Prentice-Hall, Inc., Upper Saddle River, NJ, 1982
• 29: Donald Perlis , Jack Minker, The SUPREM architecture: a new intelligent paradigm, Artificial Intelligence, v.28 n.1, p.29-42, Feb. 1986 [doi>10.1016/0004-3702(86)90029-9]
• 30: Yehoshua Sagiv, On computing restricted projections of representative instances, Proceedings of the fourth ACM SIGACT-SIGMOD symposium on Principles of database systems, p.171-180, March 25-27, 1985, Portland, Oregon, United States [doi>10.1145/325405.325427]
• 31: SCHLIPF, J.S. How uncomputable is general circumscription. In Proceedings of the 1st IEEE Conference on Logic in Computer Science. IEEE, New York, 1986, pp. 92-95.
• 32: Moshe Y Vardi, Querying logical databases, Journal of Computer and System Sciences, v.33 n.2, p.142-160, Oct. 1986 [doi>10.1016/0022-0000(86)90016-4]
• 33: Moshe Y. Vardi, Decidability and undecidability results for boundedness of linear recursive queries, Proceedings of the seventh ACM SIGACT-SIGMOD-SIGART symposium on Principles of database systems, p.341-351, March 1988, Austin, Texas, United States [doi>10.1145/308386.308470]

INDEX TERMS

Primary Classification:
  I. Computing Methodologies
  I.2 ARTIFICIAL INTELLIGENCE
      I.2.3 Deduction and Theorem Proving
          Subjects: Nonmonotonic reasoning and belief revision

Additional Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES

  I. Computing Methodologies
  I.2 ARTIFICIAL INTELLIGENCE
      I.2.3 Deduction and Theorem Proving
          Subjects: Logic programming

General Terms:
Algorithms, Design, Performance, Theory

Keywords:
Circumscription, Horn, Model checking, NP-completeness, first-order logic, nonmonotonic reasoning, undecidability