Negative Ordered Hyper-Resolution as a Proof Procedure for Disjunctive Logic Programming

• Autorzy: Nguyen L.A. L.A.
• Języki publikacji: EN

Abstrakty

EN

We prove that negative hyper-resolution using any liftable and well-founded ordering refinement is a sound and complete procedure for answering queries in disjunctive logic programs. In our formulation, answers of queries are defined using disjunctive substitutions, which are more flexible than answer literals used in theorem proving systems.

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2006
• Tom: Vol. 70, nr 4
• Strony: 351--366
• Opis fizyczny: bibliogr. 17 poz.

Twórcy

autor

Nguyen L.A. L.A.

• Institute of Informatics University of Warsaw ul. Banacha 2, 02-097 Warsaw, Poland,

Bibliografia

• [1] Apt, K., van Emden, M.: Contributions to the Theory of Logic Programming, Journal of the ACM, 29(3), 1982, 841-862.
• [2] Baumgartner, P., Furbach, U.: Calculi for Disjunctive Logic Programming, Proc. of ILPS 1997 (J. Maluszynski, Ed.), The MIT Press, 1997.
• [3] Brass, S., Lipeck, U.: Generalized Bottom-up Query Evaluation, Advances in Database Technology - EDBT'92, 3rd Int. Conf. (G. G. A. Pirotte, C. Delobel, Ed.), LNCS 580, Springer-Verlag, 1992.
• [4] Chang, C.-L., Lee, R. C.-T.: Symbolic Logic and Mechanical Theorem Proving, Academic Press, 1973.
• [5] van Emden, M., Kowalski, R.: The Semantics of Predicate Logic as a Programming Language, Journal of the ACM, 23(4), 1976, 733-742.
• [6] Green, C.: Theorem Proving by Resolution as Basis for Question-Answering Systems, Machine Intelligence, 4, 1969, 183-205.
• [7] Kowalski, R.: Predicate Logic as a Programming Language, Information Processing Letters, 74, 1974, 569-574.
• [8] Kunen, K.: The Semantics of Answer Literals, Journal of Automated Reasoning, 17(1), 1996, 83-95.
• [9] Lloyd, J.: Foundations of Logic Programming, Second Edition, Springer-Verlag, 1987.
• [10] Lobo, J., Minker, J., Rajasekar, A.: Foundations of Disjunctive Logic Programming, MIT Press, 1992.
• [11] Lobo, J., Rajasekar, A., Minker, J.: Semantics of Horn and Disjunctive Logic Programs, Theoretical Computer Science, 86(1), 1991, 93-106.
• [12] Loveland, D.: Near-Horn Prolog, Proc. of the 4th Int. Conf. on Logic Programming (J.-L. Lassez, Ed.), The MIT Press, 1987.
• [13] Luckham, D., Nilsson, N.: Extracting Information from Resolution Proof Trees, Artificial Intelligence, 2, 1971, 27-54.
• [14] Minker, J., Rajasekar, A.: A Fixpoint Semantics for Disjunctive Logic Programs, Journal of Logic Programming, 9(1), 1990, 45-74.
• [15] Nguyen, L.: Negative Hyper-Resolution as Procedural Semantics of Disjunctive Logic Programs, Proceedings of JELIA 2004, LNCS 3229 (J. Alferes, J. Leite, Eds.), Springer, 2004.
• [16] Robinson, J.: Automatic Deduction with Hyper-Resolution, International Journal of Computer Mathematics, 1, 1965, 227-234.
• [17] Robinson, J.: A Machine-Oriented Logic Based on the Resolution Principle, Journal of the ACM, 12(1), 1965, 23-41.