iBet uBet web content aggregator. Adding the entire web to your favor.
iBet uBet web content aggregator. Adding the entire web to your favor.



Link to original content: https://doi.org/10.1007/BF01178578
Contextual rewriting as a sound and complete proof method for conditional LOG-specifications | Acta Informatica Skip to main content
Springer Nature Link
Log in

Contextual rewriting as a sound and complete proof method for conditional LOG-specifications

  • Published:
Acta Informatica Aims and scope Submit manuscript

Abstract

In this paper we provide foundations to contextual rewriting. We present the class of LOG-specifications, which may be seen, essentially, as a variety of conditional specifications, which may be seen, essentially, as a of LOG-specifications are LOG-algebras, i.e. algebras satisfying that their boolean part coincides with the boolean algebra of two elements. With respect to this semantics, a proof-system called L is presented characterizing logical consequence proof-theoretically. Then, we show that, under adequate assumptions of confluence and finite termination, contextual rewriting is a complete method for this kind of specifications.

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

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

  1. Arbib, M.E., Manes, E.G.: Arrows, structures and functors: the categorical imperative. New York: Academic Press 1975

    Google Scholar 

  2. Bell, J.L., Slomson, A.B.: Models and ultraproducts: an introduction. Amsterdam: North-Holland 1971

    Google Scholar 

  3. Bergstra, J.A., Klop, J.W.: Conditional rewrite rules: confluence and termination. J. Comput. Syst. Sci.32, 323–362 (1986)

    Google Scholar 

  4. Bergstra, J.A., Tucker, J.V.: A characterization of computable data types by means of a finite, equational specification method. Proceedings 7th ICALP, Noordwijkerhout (Holland). (Lect. Notes Comput. Sci., vol. 85, pp. 76–90) Berlin Heidelberg New York: Springer 1980

    Google Scholar 

  5. Bertling, H., Ganzinger, H., Schafers, R.: CEC: a system for conditional equational completion. User Manual (Version 1.0). Report, PROSPECTRA-Project, University of Dortmund, 1988

  6. Bousdira, W., Remy, J.L.: Hierarchical contextual rewriting with several levels. Proceedings 5th Symposium on Theoretical Aspects of Computer Science, Berlin (Lect. Notes Comput. Sci., vol. 294, pp. 193–206) Berlin Heidelberg New York: Springer 1988

    Google Scholar 

  7. Brand, D., Darringuer, J.A., Joyner, W.H.: Completeness of conditional reductions. IBM T.J. Watson Res. Center Rep. RC-7404 (1978)

  8. Drosten, K.: Towards executable specification using conditional axioms. T.U. Braunschweig Rep. 83-01 (1983)

  9. Ehrig, H., Mahr, B.: Fundamentals of algebraic specification 1. (EATCS Monogr. Theor. Comput. Sci., vol. 6) Berlin Heidelberg New York: Springer 1985

    Google Scholar 

  10. Futatsugi, K., Goguen, J.A., Jouannaud, J.-P., Meseguer, J.: Principles of OBJ2. Proceedings 12th ACM Symposium on Principles of Programming Languages, New Orleans, pp. 52–66 (1985)

  11. Ganzinger, H.: Ground term confluence in parametric conditional equational specifications. Proceedings 4th Symposium on Theoretical Aspects of Computer Science, Passau, RFA (Lect. Notes Comput. Sci., vol. 247, pp. 286–298) Berlin Heidelberg New York: Springer 1987

    Google Scholar 

  12. Ganzinger, H.: Completion with history-dependent complexities for generated equations. University of Dortmund. 1988 (Lect. Notes Comput. Sci., vol. 332, pp. 73–91) Berlin Heidelberg New York: Springer 1988

    Google Scholar 

  13. Goguen, J.A., Thatcher, J.W., Wagner, E.G.: An initial algebra approach to the specification, correctness and implementation of abstract data types. In: Yeh, R.T. (ed.) Current trends in programming methodology, IV: Data Structuring, pp. 80–149. Englewood Cliffs, NJ: Prentice-Hall 1978

    Google Scholar 

  14. Goguen, J.A., Meseguer, J.: Completeness of many-sorted equational logic. Sigplan Notices16, 24–32 (1981)

    Google Scholar 

  15. Goguen, J.A., Meseguer, J.: Universal realization, persistent interconnection and implementation of abstract modules. Proceedings IX ICALP (Lect. Notes Comput. Sci., vol. 140, pp. 265–281) Berlin Heidelberg New York: Springer 1982

    Google Scholar 

  16. Goguen, J.A., Meseguer, J.: Equality, types modules and (why not?) generics for logic programming. J. Logic Program.1, 179–210 (1984)

    Google Scholar 

  17. Huet, G., Oppen, D.C.: Equations and rewrite rules: a survey. In: Book, R. (ed.) Formal language theory: perspectives and open problems. New York: Academic Press 1980

    Google Scholar 

  18. Jouannaud, J.P., Waldmann, B.: Reductive conditional term rewriting systems. Proceedings 3rd IFIP Conference on Formal Description of Programming Concepts, Lyngby, Denmark, 1986

  19. Kaplan, S.: Conditional rewrite rules. Theor. Comput. Sci.33, 175–193 (1984)

    Google Scholar 

  20. Kaplan, S.: Fair conditional term rewriting systems: unification, termination and confluence. In: Kreowski, H.-J. (ed.) Recent trends in data type specification. (Inf. Fachber., Bd. 116) Berlin Heidelberg New York: Springer 1985

    Google Scholar 

  21. Lankford, D.S.: Some new approaches to the theory and applications of conditional term rewriting systems. Report MTP-6, Math. Dept., Louisiana Tech. U., 1979

  22. Lescanne, P.: Computer experiments with the REVE term rewriting system generator. Proceedings 10th ACM Symposium Principles of Programming Languages. Austin, Texas, USA, 1983

  23. Makowski, J.A.: Why horn formulas matter in computer science: initial structures and generic examples. In: Ehrig, H., Floyd, Ch. (eds.) Formal methods and software development, vol. 1 (Lect. Notes Comput. Sci., vol. 186, pp. 374–387) Berlin Heidelberg New York: Springer 1985

    Google Scholar 

  24. Meseguer, J., Goguen, J.A.: Initiallity, induction and computability. In: Nivat, M., Reynolds, J. (eds.) Algebraic methods in semantics, pp. 459–540. Cambridge: Cambridge University Press 1985

    Google Scholar 

  25. Navarro, M.: Técnicas de reescritura para especificaciones condicionales. Tesis Doctoral, Bareelona, Spain, 1987

  26. Navarro, M., Orejas, F.: On the equivalence of hierarchical and non-hierarchical rewriting on conditional term rewriting systems. EUROSAM 84 (Lect. Notes Comput. Sci., vol. 174, pp. 74–85) Berlin Heidelberg New York: Springer 1984

    Google Scholar 

  27. Navarro, M., Orejas, F.: Parameterized horn clause specifications: proof theory and correctness. TAPSOFT '87, Pisa (Lect. Notes Comput. Sci., vol. 249, pp. 202–216) Berlin Heidelberg New York: Springer 1987

    Google Scholar 

  28. Nieuwenhuis, R., Orejas, F.: Clausal rewriting. Proceedings 2nd International Workshop on Conditional and Typed Rewriting Systems. (Lect. Notes Comput. Sci., vol. 516, pp. 246–261) Berlin Heidelberg New York: Springer 1990

    Google Scholar 

  29. Nieuwenhuis, R., Orejas, F., Rubio, A.: TRIP: an implementation of clausal rewriting. Proceedings 10th International Conference on Automated Deduction. (Lect. Notes Comput. Sci., vol. 449, pp. 667–668) Berlin Heidelberg New York: Springer 1990

    Google Scholar 

  30. Orejas, F.: On the power of conditional specifications. Sigplan Notices14, 7 (1979)

    Google Scholar 

  31. Padawitz, P.: Computing in horn clause theories (EATCS Monogr. Theor. Comput. Sci., vol. 16) Berlin Heidelberg New York: Springer 1988

    Google Scholar 

  32. Pletat, U., Engels, G., Ehrich, H-D.: Operational semantics of algebraic specifications with conditional equations. Dormunt Univ. Rep. 118/81, 1981

  33. Ponasse, D., Carrega, J.C.: Algebre et topologie booleennes Paris: Masson 1979

    Google Scholar 

  34. Remy, J.-L.: Etudes des systemes de reecriture conditionnels et applications aux types abstraits algebriques. These d'Etat, C.R.I. Nancy, 1982

    Google Scholar 

  35. Remy, J.-L.: Proving conditional identities by equational case reasoning, rewriting and normalization. Tech. Rep. C.R.I. Nancy, 1982

  36. Remy, J.-L.: A review of several closure properties in universal algebra and first order logic. CRI Nancy Rep. 85-R-081 (1985)

  37. Remy, J.-L., Zhang, H.: REVEUR 4: a system for validating conditional algebraic specifications of abstract data types. Proceedings 6th E.C.A.I. Pisa, 1984

  38. Sanella, D., Wirsing, M.: A kernel language for algebraic specification and implementation. Proceedings FCT, Bergholm, 1983

  39. Selman, A.: Completeness of calculi for axiomatically defined classes of algebras. Algebra Univers.2, 20–32 (1972)

    Google Scholar 

  40. Thatcher, J.W., Wagner, E.G., Wright, J.B.: Specification of abstract data types using conditional axioms. IBM T.J. Watson Res. Center Rep. RC-6214 (1976)

  41. Thatcher, J.W., Wagner, E.G., Wright, J.B.: Data type specification: parameterization and the power of specification techniques. ACM TOPLAS4, 711–732 (1982)

    Google Scholar 

  42. Wagner, E.G., Ehrig, H.: Canonical constraints for parameterized data types. Theor. Comput. Sci.50, 323–349 (1987)

    Google Scholar 

  43. Zhang, H.: REVEUR 4: etude et mise en œuvre de la reecriture conditionnelle. Thèse de 3ème cycle. Nancy, France, 1984

  44. Zhang, H., Remy, J.-L.: Contextual rewriting. Proceedings Conference on Rewriting Techniques and Applications, Dijon (Lect. Notes Comput. Sci., vol. 202) Berlin Heidelberg New York: Springer 1985

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Facultad de Informática, UPV-EHU, Apdo. 649, E-20080, San Sebastian, Spain

    Marisa Navarro

  2. Facultat d'Informática, UPC, Pau Gargallo 5, E-08028, Barcelona, Spain

    Fernando Orejas

  3. CRIN (CNRS and Universities of Nancy) and INRIA-Lorraine, BP 239, F-54506, Vandœvre Cedex, France

    Jean-Luc Remy

Authors
  1. Marisa Navarro
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Fernando Orejas
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Jean-Luc Remy
    View author publications

    You can also search for this author in PubMed Google Scholar

Additional information

This work was partially done during the first author's stay at C.R.I.N., with financial support of the Spain-France Integrated Action 34/212. Research partially supported by a subcontract with SESA-Alcatel under the ESPRIT program in the project PROSPECTRA, ref # 390.

Rights and permissions

Reprints and permissions

About this article

Cite this article

Navarro, M., Orejas, F. & Remy, JL. Contextual rewriting as a sound and complete proof method for conditional LOG-specifications. Acta Informatica 30, 147–180 (1993). https://doi.org/10.1007/BF01178578

Download citation

  • Received:

  • Issue Date:

  • DOI: https://doi.org/10.1007/BF01178578

Keywords

Search

Navigation