Acyclic programs
Tóm tắt
We study here a natural subclass of the locally stratified programs which we call acyclic. Acyclic programs enjoy several natural properties. First, they terminate for a large and natural class of general goals, so they could be used as terminating PROLOG programs. Next, their semantics can be defined in several equivalent ways. In particular we show that the immediate consequence operator of an acyclic programP has a unique fixpointM
p
, which coincides with the perfect model ofP, is the unique Herbrand model of the completion ofP and can be identified with the unique fixpoint of the 3-valued immediate consequence operator associated withP. The completion of an acylic programP is shown to satisfy an even stronger property: addition of a domain closure axiom results in a theory which is complete and decidable with respect to a large class of formulas including the variable-free ones. This implies thatM
p
is recursive. On the procedural side we show that SLS-resolution and SLDNF-resolution for acyclic programs coincide, are effective, sound and (non-floundering) complete with respect to the declarative semantics. Finally, we show that various forms of temporal reasoning, as exemplified by the so-called Yale Shooting Problem, can be naturally described by means of acyclic programs.
Tài liệu tham khảo
Apt, K. R., “Logic Programming,” inHandbook of Theoretical Computer Science, Vol. B (J. van Leeuwen, ed.), Elsevier, Amsterdam, pp. 493–574, 1990.
Apt, K. R. and Blair, H. A., “Arithmetic Classification of Perfect Models of Stratified Programs,”Fundamenta Informaticae, 13, pp. 1–18, 1990 (with an addendum in vol. 14, pp. 339–343, 1991).
Apt, K. R., Blair H. A. and Walker, A, “Towards a Theory of Declarative Knowledge,” inFoundations of Deductive Databases and Logic Programming (J. Minker, ed.), Morgan Kaufmann, Los Altos, pp. 89–148, 1988.
Bezem, M., “Characterizing Termination of Logic Programs with Level Mappings,” inProc. North American Conference on Logic Programming, Cleveland, Ohio, pp. 69–80, 1989.
Bidoit, N. and Froidevaux, C., “General Logical Databases and Programs: Default Logic Semantics and Stratification,”Information and Computation, 91, pp. 15–54, 1991.
Bol, R., “Loop Checking and Negation,”Report CS-R9075, Centre for Mathematics and Computer Science, Amsterdam, 1990.
Cavedon, L., “Continuity, Consistency, and Completeness Properties for Logic Programs,” inProc. of the 6th International Conference on Logic Programming, The MIT Press, pp. 571–584, 1989.
Clark, K. L., “Negation as Failure,” inLogic and Data Bases, (H. Gallaire and J. Minker, eds.), Plenum Press, New York, pp. 293–322, 1978.
Dershowitz, N., “Termination of Rewriting,”Journal of Symbolic Computation, 3, pp. 69–116, 1987.
Elkan, C., “A Perfect Logic for Reasoning about Action,”manuscript, University of Toronto, 1989.
Evans, C., “Negation-as-Failure as an Approach to the Hanks and McDermott Problem,” inProc. of the 2nd International Symposium on Artificial Intelligence, Monterrey, Mexico, 1989.
Fitting, M., “A Kripke-Kleene Semantics for General Logic Programs,”Journal of Logic Programming, 2, pp. 295–312, 1985.
Gelfond, M., “Autoepistemic Logic and Formalization of Commonsense Reasoning,” inProc. 2nd Workshop on Nonmonotonic Reasoning, Lecture Notes in Artificial Intelligence, Springer-Verlag, Berlin, 1988.
Hanks, S. and McDermott, D., “Nonmonotonic Logic and Temporal Projection,”Artificial Intelligence, 33, pp. 379–412, 1987.
Kleene, S. C.,Introduction to Metamathematics, van Nostrand, New York, 1952.
Kunen, K., “Signed Data Dependencies in Logic Programs,”Journal of Logic Programming, 7, pp. 231–246, 1989.
Lloyd, J. W.,Foundations of Logic Programming, 2nd Edition, Springer-Verlag, Berlin, 1987.
Lifschitz, V., “Computing Circumscription,” inProc. IJCAI-85, pp. 121–127, 1985.
Lifschitz, V., “Formal Theories of Action,” inThe Frame Problem in Artificial Intelligence (F. Brown, ed.), Morgan Kaufmann, Los Altos, California, 1987.
Maher, M. J., “Complete Axiomatizations of the Algebras of Finite, Rational and Infinite Trees,” inProc. of the 3rd Annual Symposium on Logic in Computer Science, Edinburgh, pp. 348–357, 1988.
Malcev, A., “Axiomatizable Classes of Locally Free Algebras of Various Types,” inThe Metamathematics of Algebraic Systems: Collected Papers, Chapter 23, North-Holland, Amsterdam, pp. 262–281, 1971.
McCarthy, J., “Circumscription—A Form of Non-Monotonic Reasoning,”Artificial Intelligence, 13, pp. 27–39, 1980.
McCarthy, J. and Hayes, P. J., “Some Philosophical Problems from the Standpoint of Artificial Intelligence,” inMachine Intelligence 4 (B. Meltzer and D. Mitchie, es.) Edinburgh University Press, Edinburgh, pp. 463–502, 1969.
Morris, P., “Curing Anomalous Extensions,” inProc. of AAAI, pp. 437–442, 1987.
Przymusinski, T. C., “On the Declarative Semantics of Deductive Databases and Logic Programs,” inFoundations of Deductive Databases and Logic Programming (J. Minker, ed.), Morgan Kaufmann Publishers, Los Altos, pp. 193–216, 1988.
Przymusinski, T. C., “On the Declarative and procedural Semantics of Logic Programs,”Journal of Automated Reasoning, 5, pp. 167–205, 1989.
Przymusinski, T. C., “Every Logic Program Has a Natural Stratification and an Iterated Least Fixed Point Model,” inProc. Principles of Database Systems (PODS’89), Philadelphia, 1989.
Shepherdson, J. C., “Negation in Logic Programming,” inFoundations of Deductive Databases and Logic Programming (J. Minker, ed.), Morgan Kaufmann Publishers, Los Altos, pp. 19–88, 1988.
Shoenfield, J. R.,Mathematical Logic, Addison-Wesley, Reading MA, 1967.