Skip to main content
SpringerLink
Log in

Negation with logical variables in conditional rewriting

  • Regular Papers
  • Conference paper
  • First Online:
Rewriting Techniques and Applications (RTA 1989)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 355))

Included in the following conference series:

Abstract

We give a general formalism for conditional rewriting, with systems containing conditional rules whose antecedents contain literals to be shown satisfiable and/or unsatisfiable. We explore semantic issues, addressing when the associated operational rewriting mechanism is sound and complete. We then give restrictions on the formalism which enable us to construct useful and meaningful specifications using the proposed operational mechanism.

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.

References

  1. J.C.M. Baeten, J.A. Bergstra, J.W. Klop, Term Rewriting Systems with Priorities, Proc. 2nd RTA Conf., Bourdeaux, Springer-Verlag LNCS 256, pp83–94, 1987.

    Google Scholar 

  2. D.Brand, J.A.Darringer, W.Joyner, Completeness of Conditional Reductions, IBM Res. Rep. RC7404, 1978.

    Google Scholar 

  3. J.A. Bergstra, J.W. Klop, Conditional Rewrite Rules: Confluency and Termination, JCSS 32, pp.323–362, 1986.

    Google Scholar 

  4. K.L. Clark, Negation as Failure, in Logic and Databases, H. Gallaire & J. Minker (eds.), Plenum, NY, pp293–322, 1978.

    Google Scholar 

  5. C.L. Chang, R.C. Lee, Symbolic Logic and Mechanical Theorem Proving, Academic Press, New York, 1973.

    Google Scholar 

  6. H. Comon, Sufficient Completeness, Term Rewriting Systems, and “Anti-Unification”, Proc. 8th CADE, Springer-Verlag LNCS 230, pp128–140, 1986.

    Google Scholar 

  7. N. Dershowitz, Termination of Rewriting, Proc. First RTA Conf., Dijon, Springer-Verlag LNCS 202, pp180–224, 1985.

    Google Scholar 

  8. D. DeGroot, G. Lindstrom, Logic Programming: Functions, Relations and Equations, Prentice Hall (NJ), 1986.

    Google Scholar 

  9. N. Dershowitz, D.A. Plaisted, Logic Programming cum Applicative Programming, Proc. 1985 Symp. on Logic Programming, Boston, 1985.

    Google Scholar 

  10. M. Fay, First-Order Unification in an Equational Theory, Proc. 4th CADE, Austin (Texas), 1979, pp161–167.

    Google Scholar 

  11. M. Fitting, A Kripke-Kleene Semantics for Logic Programs, The Journal of Logic Programming, vol.4, Elsevier Science Pub., 1985, pp295–312.

    Google Scholar 

  12. L. Fribourg, Oriented Equational Clauses as a Programming Language, Proc. 11th ICALP, Antwerp (Belgium), July 1984.

    Google Scholar 

  13. J.A. Goguen, J. Meseguer, Equality, Types, Modules and Generics for Logic Programming, J. of Logic Programming, Vol. 1, No.2, 1984, pp179–210.

    Google Scholar 

  14. G. Huet, D.S. Oppen, Equations and Rewrite Rules: A Survey, Tech.Rep. CSL-111, SRI Int'l., California, 1980.

    Google Scholar 

  15. J.M. Hullot, Canonical Forms and Unification, Proc. 5th CADE, Springer-Verlag LNCS 87, April 1980.

    Google Scholar 

  16. H. Hussmann, Unification in Conditional-Equational Theories, Proc. EUROCAL Conf. at Linz (Austria), Springer-Verlag, LNCS 204, Apr. 1985, pp543–553.

    Google Scholar 

  17. J.-P. Jouannaud, E. Kounalis, Proofs by Induction in Equational Theories without Constructors, Symp. on Logic in C.S., Cambridge (Mass.), USA, 1986, pp358–366.

    Google Scholar 

  18. J.-P. Jouannaud, B. Waldmann, Reductive Conditional Term Rewriting Systems, Proc. Third TC2 Working Conf. on the Formal Description of Prog. Concepts, Ebberup, Denmark, Aug. 1986.

    Google Scholar 

  19. S. Kaplan, Fair Conditional Term Rewriting Systems: Unification, Termination and Confluence, Res.Rep. 194, Universite de Paris-Sud, Orsay, Nov. 1984.

    Google Scholar 

  20. S. Kaplan, Positive/Negative Conditional Rewriting, Proc. First Int'l. Workshop on Conditional Term Rewriting Systems, Orsay, Springer-Verlag LNCS 308, 1988, pp129–143.

    Google Scholar 

  21. S.Kaplan, J.-P.Jouannaud (eds.), Proc. First Int'l. Workshop on Conditional Term Rewriting Systems, Orsay, Springer-Verlag LNCS 308, 1988.

    Google Scholar 

  22. E. Kounalis, Completeness in Data Type Specifications, Res. Rep. 84-R-92, C.R.I.N., Nancy (France) 1984.

    Google Scholar 

  23. R.A. Kowalski, Predicate Logic as a Programming Language, Information Processing 74, North Holland, Apr. 1974, pp556–574.

    Google Scholar 

  24. D.S.Lankford, Canonical Inference, Rep. ATP-32, Dept. of Math. & C.S., Univ. of Texas at Austin, Dec. 1975.

    Google Scholar 

  25. D.S. Lankford, Some New Approaches to the Theory and Applications of Conditional Term Rewriting Systems, Research Report MTP-6, Univ. of Louisiana, Ruston, 1979.

    Google Scholar 

  26. G. Lindstrom, Functional Programming and the Logical Variable, Proc. ACM POPL Symp., Jan. 1985.

    Google Scholar 

  27. C.K.Mohan, Negation in Equational Reasoning and Conditional Specifications, Ph.D. Thesis, State University of New York at Stony Brook, 1988.

    Google Scholar 

  28. C.K.Mohan, Priority Rewriting: Semantics, Confluence and Conditionals, Proc. 3rd RTA Conf., Chapel Hill, 1989.

    Google Scholar 

  29. C.K. Mohan, M.K. Srivas, Function Definitions in Term Rewriting and Applicative Programming, Information and Control, Academic Press, New York, Vol.71, No.3, Dec. 1986, pp186–217.

    Google Scholar 

  30. C.K. Mohan, M.K. Srivas, Conditional Specifications with Inequational Assumptions, Proc. First Int'l. Workshop on Conditional Term Rewriting Systems, Orsay, Springer-Verlag LNCS 308, 1988, pp161–178.

    Google Scholar 

  31. C.K.Mohan, M.K.Srivas, D.Kapur, Inference Rules and Proof Procedures for Inequations, (to appear) Journal of Logic Programming, 1989.

    Google Scholar 

  32. M.L. Navarro, Tecnicas de Reescritura para especificaciones condicionales, These Doctorale de l'Universite Polytechnique de Catalunya, Barcelona (Spain), 1987.

    Google Scholar 

  33. U. Pletat, G. Engels, H.D. Ehrich, Operational Semantics of Algebraic Specifications with Conditional Equations, 7eme C.A.A.P., Lille (France), 1982.

    Google Scholar 

  34. U. Reddy, Narrowing as the Operational Semantics of Functional Languages, Proc. IEEE Logic Programming Symp., Boston, 1985.

    Google Scholar 

  35. R. Reiter, On Closed World Data Bases, in Logic and Data Bases, H. Gallaire & J. Minker (eds.), Plenum, NY, 1978.

    Google Scholar 

  36. J.-L. Remy, Etudes des systemes de reecriture conditionnels et application aux types abstraits algebriques, These d'Etat, Nancy (France), 1982.

    Google Scholar 

  37. P. Rety, Improving Basic Narrowing Techniques, Proc. 2nd RTA Conf., Bourdeaux, Springer-Verlag LNCS 256, pp228–241, 1987.

    Google Scholar 

  38. J.R. Slagle, Automated Theorem-Proving for Theories with Simplifiers, Commutativity and Associativity, J. ACM, Vol.21, No.4, 1974, pp622–642.

    Google Scholar 

  39. J.J.Thiel, Stop Losing Sleep over Incomplete Specifications, Proc. 11th ACM POPL Symp., 1983.

    Google Scholar 

  40. H. Zhang, J.L. Remy, Contextual Rewriting, Proc. Conf. on Rewriting Techniques and Applications, Dijon (France), Springer-Verlag, LNCS 202, June 1985.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. School of Computer & Info. Sci., Syracuse University, 13244-4100, Syracuse, NY

    Chilukuri K. Mohan

  2. Odyssey Research Associates, Inc., 301 A Harris B. Dates Drive, 14850-1313, Ithaca, NY

    Mandayam K. Srivas

Authors
  1. Chilukuri K. Mohan
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Mandayam K. Srivas
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Nachum Dershowitz

Rights and permissions

Reprints and permissions

Copyright information

© 1989 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Mohan, C.K., Srivas, M.K. (1989). Negation with logical variables in conditional rewriting. In: Dershowitz, N. (eds) Rewriting Techniques and Applications. RTA 1989. Lecture Notes in Computer Science, vol 355. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-51081-8_115

Download citation

  • DOI: https://doi.org/10.1007/3-540-51081-8_115

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-51081-9

  • Online ISBN: 978-3-540-46149-4

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation