Abstract
This paper presents an alternative view on propositional disjunctive logic program: Disjunctive program = Control program + Horn program. For this we introduce a program transformation which transforms a disjunctive logic program into a Horn program and a so called control program. The control program consists of only disjunctions of new propositional atoms and controls the “execution” of the Horn program. The relationship between original and transformed programs is established by using circumscription. Based on this relationship a new minimal model reasoning approach is developed. Due to the transformation it is straightforward to incorporate SLD-resolution into the proof procedure.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Chandrabose Aravindan. An abductive framework for negation in disjunctive logic programming. In J. J. Alferes, L. M. Pereira, and E. Orlowska, editors, Proceedings of Joint European workshop on Logics in AI, number 1126 in Lecture Notes in Artificial Intelligence, pages 252–267. Springer-Verlag, 1996. A related report is available on the web from <http://www.unikoblenz.de/~arvind/papers/>.
Peter Baumgartner and Ulrich Furbach. PROTEIN: A PROver with a Theory Extension I nterface. In A. Bundy, editor, Automated Deduction-CADE-12, volume 814 of Lecture Notes in Artificial Intelligence, pages 769–773. Springer, 1994. Available in the WWW, URL: http://www.uni-koblenz.de/ag-ki/Systems/PROTEIN/.
Peter Baumgartner and Ulrich Furbach. Calculi for Disjunctive Logic Programming. In Jan Maluszynski, editor, Logic Programming-Proceedings of the 1997 International Symposium, Port Jefferson, New York, 1997. The MIT Press.
Peter Baumgartner, Ulrich Furbach, and Ilkka Niemelä. Hyper Tableaux. In Proc. JELIA 96, number 1126 in Lecture Notes in Artificial Intelligence. European Workshop on Logic in AI, Springer, 1996.
Peter Baumgartner, Ulrich Furbach, and Frieder Stolzenburg. Computing Answers with Model Elimination. Artificial Intelligence, 90(1–2):135–176, 1997.
Matthew L. Ginsberg. A circumscriptive theorem prover. Artificial Intelligence, 39:209–230, 1989.
M. Gelfond, H. Przymusinska, and T. Przymusinski. On the relationship between circumscription and negation as failure. Artificial Intelligence, 38:75–94, 1989.
K. Inoue, M. Koshimura, and R. Hasegawa. Embedding negation as failure into a model generation theorem prover. In The 11th International Conference on Automated Deduction, pages 400–415, Saratoga Springs, NY, USA, June 1992. Springer-Verlag.
V. Lifschitz. Computing circumscription. In Proceedings of the 9th International Joint Conference on Artificial Intelligence, pages 121–127, Los Angeles, California, USA, August 1985. Morgan Kaufmann Publishers.
J. W. Lloyd. Foundations of Logic Programming. Springer-Verlag, second extended edition, 1987.
Jorge Lobo, Jack Minker, and Arcot Rajasekar. Foundations of disjunctive logic programming. MIT Press, 1992.
D. Loveland. Near-Horn Prolog and Beyond. Journal of Automated Reasoning, 7:1–26, 1991.
D. Loveland, D. Reed, and D. Wilson. SATCHMORE: SATCHMO with RElevance. Journal of Automated Reasoning, 14:325–351, 1995.
Wenjin Lu. Minimal model generation based on e-hyper tableau. In Cristopher Habel Gerhard Brewka and Bernhard Nebel, editors, Proceedings of KI’97, number 1303 in Lecture Notes in Artificial Intelligence, pages 99–110. Springer-Verlag, 1997.
Rainer Manthey and François Bry. SATCHMO: a theorem prover implemented in Prolog. In Ewing Lusk and Ross Overbeek, editors, Proceedings of the 9 th Conference on Automated Deduction, Argonne, Illinois, May 1988, volume 310 of Lecture Notes in Computer Science, pages 415–434. Springer, 1988.
J. McCarthy. Circumscription—a form of non-monotonic reasoning. Artificial Intelligence, 13:27–39, 1980.
Jack Minker. On indefinite databases and the closed world assumption. In Lecture Notes in Computer Science 138, pages 292–308. Springer-Verlag, 1982.
I. Niemelä. A tableau calculus for minimal model reasoning. In Proceedings of the Fifth Workshop on Theorem Proving with Analytic Tableaux and Related Methods, pages 278–294, Terrasini, Italy, May 1996. Springer-Verlag.
A. Nerode, R.T. Ng, and V.S. Subrahmanian. Computing circumscriptive databases: I. theory and algorithms. Information and Computation, 116:58–80, 1995.
N. Olivetti. A tableaux and sequent calculus for minimal entailment. Journal of Automated Reasoning, 9:99–139, 1992.
T.C. Przymusinski. An algorithm to compute circumscription. Artificial Intelligence, 38:49–73, 1989.
A. Yahya and L. J. Henschen. Deduction in non-horn databases. Journal of Automated Reasoning, 1(2):141–160, 1985.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1998 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Lu, W., Furbach, U. (1998). Disjunctive Logic Program = Horn Program + Control Program. In: Dix, J., del Cerro, L.F., Furbach, U. (eds) Logics in Artificial Intelligence. JELIA 1998. Lecture Notes in Computer Science(), vol 1489. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-49545-2_3
Download citation
DOI: https://doi.org/10.1007/3-540-49545-2_3
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-65141-3
Online ISBN: 978-3-540-49545-1
eBook Packages: Springer Book Archive