Conditional narrowing with constructive negation | SpringerLink
Skip to main content
Springer Nature Link
Log in

Conditional narrowing with constructive negation

  • Conference paper
  • First Online:
Extensions of Logic Programming (ELP 1992)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 660))

Included in the following conference series:

Abstract

In this paper we present a narrower for conditional equational theories whose clauses allow disequations in their bodies (normal theories). Our approach deals with disequations in a constructive manner and thus allows non ground negative queries. We give a formal operational semantics for normal theories and define the notion of completion and stratification of a normal theory. We show that there exists one minimal model for the completion of a stratified normal theory. Then we prove the correctness of the operational semantics with respect to the completion of a stratified normal theory.

The work of the first author has been partially supported by CICYT under grant TIC 92-0793. The work of the second author has been partially supported by “Progetto Finalizzato Sistemi Informatici e Calcolo Parallelo of C.N.R.” under grant n.9100880.PF69

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

References

  1. M. Alpuente and M. Falaschi. Narrowing as an Incremental Constraint Satisfaction Algorithm. In J. Maluszyński and M. Wirsing, editors, Proc. of PLILP'91, volume 528 of Lecture Notes in Computer Science, pages 111–122. Springer-Verlag, Berlin, 1991.

    Google Scholar 

  2. M. Alpuente, M. Falaschi, and G. Levi. Incremental Constraint Satisfaction for Equational Logic Programming. Technical report, Dipartimento di Informatica, Università di Pisa, 1991. To appear in Theoretical Computer Science.

    Google Scholar 

  3. K. R. Apt. Introduction to Logic Programming. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B: Formal Models and Semantics. Elsevier, Amsterdam and The MIT Press, Cambridge, 1990.

    Google Scholar 

  4. K. R. Apt, H. Blair, and A. Walker. Towards a Theory of Declarative Knowledge. In J. Minker, editor, Foundations of Deductive Databases and Logic Programming, pages 89–148. Morgan Kaufmann, Los Altos, Ca., 1988.

    Google Scholar 

  5. L. Bachmair and H. Ganzinger. On restrictions of ordered paramodulation with simplification. In E. Y. Shapiro, editor, Proc. 10th Int'l Conf. on Automated Deduction, volume 449 of Lecture Notes in Computer Science, pages 427–441, 1990.

    Google Scholar 

  6. L. Bachmair and H. Ganzinger. Perfect Model Semantics for Logic Programs with Equality. In K. Furukawa, editor, Proc. Eighth Int'l Conf. on Logic Programming, pages 645–659. The MIT Press, Cambridge, Mass., 1991.

    Google Scholar 

  7. M. Bellia and G. Levi. The relation between logic and functional languages. Journal of Logic Programming, 3:217–236, 1986.

    Google Scholar 

  8. J.A. Bergstra and J.W. Klop. Conditional Rewrite Rules: confluence and termination. Journal of Computer and System Sciences, 32:323–362, 1986.

    Google Scholar 

  9. P. Bosco, E. Giovannetti, and C. Moiso. Narrowing vs. SLD-resolution. Theoretical Computer Science, 59:3–23, 1988.

    Google Scholar 

  10. P. G. Bosco, E. Giovannetti, G. Levi, C. Moiso, and C. Palamidessi. A complete semantic characterization of K-LEAF, a logic language with partial functions. In Proc. of the Fourth IEEE Symposium on Logic Programming, pages 318–327, San Francisco, 1987. IEEE Computer Society Press, N.W., Washington.

    Google Scholar 

  11. D. Chan. Constructive Negation Based on the Completed Database. In R. A. Kowalski and K. A. Bowen, editors, Proc. Fifth Int'l Conf. on Logic Programming, pages 111–125. The MIT Press, Cambridge, Mass., 1988.

    Google Scholar 

  12. D. Chan. An Extension of Constructive Negation and its Application in Coroutining. In E. Lusk and R. Overbeck, editors, Proc. North American Conf. on Logic Programming'89, pages 477–493. The MIT Press, Cambridge, Mass., 1989.

    Google Scholar 

  13. K.L. Clark. Negation as Failure. In H. Gallaire and J. Minker, editors, Logic and data bases. Plenum Press, New York, 1978.

    Google Scholar 

  14. A. Colmerauer. Equations and Inequations on Finite and Infinite Trees. In Proc. Int'l Conf. on Fifth Generation Computer Systems, pages 85–99. ICOT, Tokio, 1984.

    Google Scholar 

  15. N. Dershowitz and A. Plaisted. Logic Programming cum Applicative Programming. In Proc. First IEEE Int'l Symp. on Logic Programming, pages 54–66. IEEE, 1984.

    Google Scholar 

  16. M. Fay. First, Order Unification in an Equational Theory. In 4th Int'l Conf. on Automated Deduction, pages 161–167, 1979.

    Google Scholar 

  17. M. Fitting. A Kripke-Kleene semantics for logic programs. In Journal of Logic Programming, volume 2, pages 295–312, 1985.

    Google Scholar 

  18. L. Fribourg. Slog: a logic programming language interpreter based on clausal superposition and rewriting. In Proc. Second IEEE Int'l Symp. on Logic Programming, pages 172–185. IEEE, 1985.

    Google Scholar 

  19. E. Giovannetti, G. Levi, C. Moiso, and C. Palamidessi. Kernel Leaf: A Logic plus Functional Language. Journal of Computer and System Sciences, 42, 1991.

    Google Scholar 

  20. J. Goguen and J. Meseguer. Eqlog: Equality, Types and Generic Modules for Logic Programming. In D. de Groot. and G. Lindstrom, editors, Logic Programming, Functions, Relations and Equations, pages 295–363. Prentice-Hall, 1986.

    Google Scholar 

  21. S. Hölldobler. Foundations of Equational Logic Programming, volume 353 of Lecture Notes in Artificial Intelligence. Springer-Verlag, Berlin, 1989.

    Google Scholar 

  22. G. Huet and D.C. Oppen. Equations and Rewrite Rules: a Survey. In Formal Languages: perspectives and open problems, pages 349–405. Academic Press, 1980.

    Google Scholar 

  23. J.M. Hullot. Canonical Forms and Unification. In 5th Int'l Conf. on Automated Deduction, volume 87 of Lecture Notes in Computer Science, pages 318–334. Springer-Verlag, Berlin, 1980.

    Google Scholar 

  24. H. Hussman. Unification in conditional-equational theories. Technical report, Fakultät für Mathematik und Informatik, Universität Passau, 1986.

    Google Scholar 

  25. J. Jaffar, J.-L. Lassez, and M.J. Maher. A logic programming language scheme. In D. de Groot and G. Lindstrom, editors, Logic Programming, Functions, Relations and Equations, pages 441–468. Prentice Hall, Englewood Cliffs, NJ, 1986.

    Google Scholar 

  26. S. Kaplan. Positive/negative conditional rewriting. In S. Kaplan and J.-P. Jouannaud, editors, Conditional Term Rewriting Systems, volume 308 of Lecture Notes in Computer Science, pages 129–143. Springer-Verlag, Berlin, 1987.

    Google Scholar 

  27. K. Kunen. Negation in logic programming. Journal of Logic Programming, 4:289–308, 1987.

    Google Scholar 

  28. J.-L. Lassez, M. J. Maher, and K. Marriott. Unification Revisited. In J. Minker, editor, Foundations of Deductive Databases and Logic Programming, pages 587–625. Morgan Kaufmann, Los Altos, Ca., 1988.

    Google Scholar 

  29. J. W. Lloyd. Foundations of Logic Programming. Springer-Verlag, Berlin, 1987. Second edition.

    Google Scholar 

  30. M. J. Maher. Complete Axiomatizations of the Algebras of Finite, Rational and Infinite Trees. In Proc. Third IEEE Symp. on Logic In Computer Science, pages 348–357. Computer Science Press, New York, 1988.

    Google Scholar 

  31. A. Middeldorp and E. Hamoen. Counterexamples to completeness results for basic narrowing. In H. Kirchner and G. Levi, editors, Proc. Third Int'l Conf. on Algebraic and Logic Programming, volume 632 of Lecture Notes in Computer Science, pages 244–258. Springer-Verlag, Berlin, 1992.

    Google Scholar 

  32. J.J. Moreno and M. Rodriguez-Artalejo. BABEL: A Functional and Logic Programming Language based on a constructor discipline and narrowing. In I. Grabowski, P. Lescanne, and W. Wechler, editors, Algebraic and Logic Programming, volume 343 of Lecture Notes in Computer Science, pages 223–232. Springer-Verlag, Berlin, 1988.

    Google Scholar 

  33. W. Nutt, P. Réty, and G. Smolka. Basic narrowing revisited. Journal of Symbolic Computation, 7:295–317, 1989.

    Google Scholar 

  34. M. O'Donnell. Computing in Systems Described by Equations, volume 58 of Lecture Notes in Computer Science. Springer-Verlag, Berlin, 1977.

    Google Scholar 

  35. P. Padawitz. Computing in Horn Clause Theories, volume 16 of EATCS Monographs on Theoretical Computer Science. Springer-Verlag, Berlin, 1988.

    Google Scholar 

  36. T. Przymusinski. On the Declarative Semantics of Deductive Databases and Logic Programs. In J. Minker, editor, Foundations of Deductive Databases and Logic Programming, pages 193–216. Morgan Kaufmann, Los Altos, Ca., 1988.

    Google Scholar 

  37. T. Przymusinski. On the Declarative and Procedural Semantics of Logic Programs. Journal of Automated Reasoning, 5(2):201–228, 1989.

    Google Scholar 

  38. M.J. Ramírez and M. Falaschi. Conditional narrowing with constructive negation. Technical report, Dipartimento di Informatica, Università di Pisa, 1992.

    Google Scholar 

  39. J.H. Siekmann. Universal unification. In 7th Int'l Conf. on Automated Deduction, volume 170 of Lecture Notes in Computer Science, pages 1–42. Springer-Verlag, Berlin, 1984.

    Google Scholar 

  40. P. J. Stuckey. Constructive Negation for Constraint Logic Programming. In Proc. Sixth IEEE Symp. on Logic In Computer Science. IEEE Computer Society Press, 1991.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Departamento de Sistemas Informáticos y Computación, Universidad Politécnica de Valencia, Camino de Vera s/n, Apdo. 22012, 46020, Valencia, Spain

    María José Ramírez

  2. Dipartimento di Informatica, Università di Pisa, Corso Italia 40, 56125, Pisa, Italy

    Moreno Falaschi

Authors
  1. María José Ramírez
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Moreno Falaschi
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

E. Lamma P. Mello

Rights and permissions

Reprints and permissions

Copyright information

© 1993 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Ramírez, M.J., Falaschi, M. (1993). Conditional narrowing with constructive negation. In: Lamma, E., Mello, P. (eds) Extensions of Logic Programming. ELP 1992. Lecture Notes in Computer Science, vol 660. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-56454-3_4

Download citation

  • DOI: https://doi.org/10.1007/3-540-56454-3_4

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-56454-6

  • Online ISBN: 978-3-540-47562-0

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation