{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,2]],"date-time":"2022-04-02T21:02:51Z","timestamp":1648933371771},"reference-count":44,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[1993,2,1]],"date-time":"1993-02-01T00:00:00Z","timestamp":728524800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Acta Informatica"],"published-print":{"date-parts":[[1993,2]]},"DOI":"10.1007\/bf01178578","type":"journal-article","created":{"date-parts":[[2005,2,17]],"date-time":"2005-02-17T19:36:30Z","timestamp":1108668990000},"page":"147-180","source":"Crossref","is-referenced-by-count":0,"title":["Contextual rewriting as a sound and complete proof method for conditional LOG-specifications"],"prefix":"10.1007","volume":"30","author":[{"given":"Marisa","family":"Navarro","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Fernando","family":"Orejas","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jean-Luc","family":"Remy","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"CR1","volume-title":"Arrows, structures and functors: the categorical imperative","author":"M.E. Arbib","year":"1975","unstructured":"Arbib, M.E., Manes, E.G.: Arrows, structures and functors: the categorical imperative. New York: Academic Press 1975"},{"key":"CR2","volume-title":"Models and ultraproducts: an introduction","author":"J.L. Bell","year":"1971","unstructured":"Bell, J.L., Slomson, A.B.: Models and ultraproducts: an introduction. Amsterdam: North-Holland 1971"},{"key":"CR3","doi-asserted-by":"crossref","first-page":"323","DOI":"10.1016\/0022-0000(86)90033-4","volume":"32","author":"J.A. Bergstra","year":"1986","unstructured":"Bergstra, J.A., Klop, J.W.: Conditional rewrite rules: confluence and termination. J. Comput. Syst. Sci.32, 323?362 (1986)","journal-title":"J. Comput. Syst. Sci."},{"key":"CR4","series-title":"Lect. Notes Comput. Sci.","doi-asserted-by":"crossref","first-page":"76","DOI":"10.1007\/3-540-10003-2_61","volume-title":"Proceedings 7th ICALP, Noordwijkerhout (Holland)","author":"J.A. Bergstra","year":"1980","unstructured":"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"},{"key":"CR5","unstructured":"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"},{"key":"CR6","series-title":"Lect. Notes Comput. Sci.","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1007\/BFb0035845","volume-title":"Proceedings 5th Symposium on Theoretical Aspects of Computer Science, Berlin","author":"W. Bousdira","year":"1988","unstructured":"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"},{"key":"CR7","unstructured":"Brand, D., Darringuer, J.A., Joyner, W.H.: Completeness of conditional reductions. IBM T.J. Watson Res. Center Rep. RC-7404 (1978)"},{"key":"CR8","unstructured":"Drosten, K.: Towards executable specification using conditional axioms. T.U. Braunschweig Rep. 83-01 (1983)"},{"key":"CR9","series-title":"EATCS Monogr. Theor. Comput. Sci.","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-69962-7","volume-title":"Fundamentals of algebraic specification 1","author":"H. Ehrig","year":"1985","unstructured":"Ehrig, H., Mahr, B.: Fundamentals of algebraic specification 1. (EATCS Monogr. Theor. Comput. Sci., vol. 6) Berlin Heidelberg New York: Springer 1985"},{"key":"CR10","doi-asserted-by":"crossref","unstructured":"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)","DOI":"10.1145\/318593.318610"},{"key":"CR11","series-title":"Lect. Notes Comput. Sci.","doi-asserted-by":"crossref","first-page":"286","DOI":"10.1007\/BFb0039613","volume-title":"Proceedings 4th Symposium on Theoretical Aspects of Computer Science, Passau, RFA","author":"H. Ganzinger","year":"1987","unstructured":"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"},{"key":"CR12","series-title":"Lect. Notes Comput. Sci.","doi-asserted-by":"crossref","first-page":"73","DOI":"10.1007\/3-540-50325-0_4","volume-title":"Completion with history-dependent complexities for generated equations","author":"H. Ganzinger","year":"1988","unstructured":"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"},{"key":"CR13","first-page":"80","volume-title":"Current trends in programming methodology, IV: Data Structuring","author":"J.A. Goguen","year":"1978","unstructured":"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"},{"key":"CR14","doi-asserted-by":"crossref","first-page":"24","DOI":"10.1145\/947864.947865","volume":"16","author":"J.A. Goguen","year":"1981","unstructured":"Goguen, J.A., Meseguer, J.: Completeness of many-sorted equational logic. Sigplan Notices16, 24?32 (1981)","journal-title":"Sigplan Notices"},{"key":"CR15","series-title":"Lect. Notes Comput. Sci.","doi-asserted-by":"crossref","first-page":"265","DOI":"10.1007\/BFb0012775","volume-title":"Proceedings IX ICALP","author":"J.A. Goguen","year":"1982","unstructured":"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"},{"key":"CR16","doi-asserted-by":"crossref","first-page":"179","DOI":"10.1016\/0743-1066(84)90004-9","volume":"1","author":"J.A. Goguen","year":"1984","unstructured":"Goguen, J.A., Meseguer, J.: Equality, types modules and (why not?) generics for logic programming. J. Logic Program.1, 179?210 (1984)","journal-title":"J. Logic Program."},{"key":"CR17","volume-title":"Formal language theory: perspectives and open problems","author":"G. Huet","year":"1980","unstructured":"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"},{"key":"CR18","unstructured":"Jouannaud, J.P., Waldmann, B.: Reductive conditional term rewriting systems. Proceedings 3rd IFIP Conference on Formal Description of Programming Concepts, Lyngby, Denmark, 1986"},{"key":"CR19","doi-asserted-by":"crossref","first-page":"175","DOI":"10.1016\/0304-3975(84)90087-2","volume":"33","author":"S. Kaplan","year":"1984","unstructured":"Kaplan, S.: Conditional rewrite rules. Theor. Comput. Sci.33, 175?193 (1984)","journal-title":"Theor. Comput. Sci."},{"key":"CR20","series-title":"Inf. Fachber.","volume-title":"Recent trends in data type specification","author":"S. Kaplan","year":"1985","unstructured":"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"},{"key":"CR21","unstructured":"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"},{"key":"CR22","doi-asserted-by":"crossref","unstructured":"Lescanne, P.: Computer experiments with the REVE term rewriting system generator. Proceedings 10th ACM Symposium Principles of Programming Languages. Austin, Texas, USA, 1983","DOI":"10.1145\/567067.567078"},{"key":"CR23","series-title":"Lect. Notes Comput. Sci.","doi-asserted-by":"crossref","first-page":"374","DOI":"10.1007\/3-540-15198-2_24","volume-title":"Formal methods and software development, vol. 1","author":"J.A. Makowski","year":"1985","unstructured":"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"},{"key":"CR24","first-page":"459","volume-title":"Algebraic methods in semantics","author":"J. Meseguer","year":"1985","unstructured":"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"},{"key":"CR25","unstructured":"Navarro, M.: T\u00e9cnicas de reescritura para especificaciones condicionales. Tesis Doctoral, Bareelona, Spain, 1987"},{"key":"CR26","series-title":"Lect. Notes Comput. Sci.","doi-asserted-by":"crossref","first-page":"74","DOI":"10.1007\/BFb0032832","volume-title":"EUROSAM 84","author":"M. Navarro","year":"1984","unstructured":"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"},{"key":"CR27","series-title":"Lect. Notes Comput. Sci.","doi-asserted-by":"crossref","first-page":"202","DOI":"10.1007\/3-540-17660-8_56","volume-title":"TAPSOFT '87, Pisa","author":"M. Navarro","year":"1987","unstructured":"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"},{"key":"CR28","series-title":"Lect. Notes Comput. Sci.","first-page":"246","volume-title":"Proceedings 2nd International Workshop on Conditional and Typed Rewriting Systems","author":"R. Nieuwenhuis","year":"1990","unstructured":"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"},{"key":"CR29","series-title":"Lect. Notes Comput. Sci.","doi-asserted-by":"crossref","first-page":"667","DOI":"10.1007\/3-540-52885-7_133","volume-title":"Proceedings 10th International Conference on Automated Deduction","author":"R. Nieuwenhuis","year":"1990","unstructured":"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"},{"key":"CR30","doi-asserted-by":"crossref","first-page":"7","DOI":"10.1145\/954245.954252","volume":"14","author":"F. Orejas","year":"1979","unstructured":"Orejas, F.: On the power of conditional specifications. Sigplan Notices14, 7 (1979)","journal-title":"Sigplan Notices"},{"key":"CR31","series-title":"EATCS Monogr. Theor. Comput. Sci.","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-73824-1","volume-title":"Computing in horn clause theories","author":"P. Padawitz","year":"1988","unstructured":"Padawitz, P.: Computing in horn clause theories (EATCS Monogr. Theor. Comput. Sci., vol. 16) Berlin Heidelberg New York: Springer 1988"},{"key":"CR32","unstructured":"Pletat, U., Engels, G., Ehrich, H-D.: Operational semantics of algebraic specifications with conditional equations. Dormunt Univ. Rep. 118\/81, 1981"},{"key":"CR33","volume-title":"Algebre et topologie booleennes","author":"D. Ponasse","year":"1979","unstructured":"Ponasse, D., Carrega, J.C.: Algebre et topologie booleennes Paris: Masson 1979"},{"key":"CR34","volume-title":"Etudes des systemes de reecriture conditionnels et applications aux types abstraits algebriques","author":"J.-L. Remy","year":"1982","unstructured":"Remy, J.-L.: Etudes des systemes de reecriture conditionnels et applications aux types abstraits algebriques. These d'Etat, C.R.I. Nancy, 1982"},{"key":"CR35","unstructured":"Remy, J.-L.: Proving conditional identities by equational case reasoning, rewriting and normalization. Tech. Rep. C.R.I. Nancy, 1982"},{"key":"CR36","unstructured":"Remy, J.-L.: A review of several closure properties in universal algebra and first order logic. CRI Nancy Rep. 85-R-081 (1985)"},{"key":"CR37","unstructured":"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"},{"key":"CR38","doi-asserted-by":"crossref","unstructured":"Sanella, D., Wirsing, M.: A kernel language for algebraic specification and implementation. Proceedings FCT, Bergholm, 1983","DOI":"10.1007\/3-540-12689-9_122"},{"key":"CR39","doi-asserted-by":"crossref","first-page":"20","DOI":"10.1007\/BF02945004","volume":"2","author":"A. Selman","year":"1972","unstructured":"Selman, A.: Completeness of calculi for axiomatically defined classes of algebras. Algebra Univers.2, 20?32 (1972)","journal-title":"Algebra Univers."},{"key":"CR40","unstructured":"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)"},{"key":"CR41","doi-asserted-by":"crossref","first-page":"711","DOI":"10.1145\/69622.357192","volume":"4","author":"J.W. Thatcher","year":"1982","unstructured":"Thatcher, J.W., Wagner, E.G., Wright, J.B.: Data type specification: parameterization and the power of specification techniques. ACM TOPLAS4, 711?732 (1982)","journal-title":"ACM TOPLAS"},{"key":"CR42","doi-asserted-by":"crossref","first-page":"323","DOI":"10.1016\/0304-3975(87)90119-8","volume":"50","author":"E.G. Wagner","year":"1987","unstructured":"Wagner, E.G., Ehrig, H.: Canonical constraints for parameterized data types. Theor. Comput. Sci.50, 323?349 (1987)","journal-title":"Theor. Comput. Sci."},{"key":"CR43","unstructured":"Zhang, H.: REVEUR 4: etude et mise en ?uvre de la reecriture conditionnelle. Th\u00e8se de 3\u00e8me cycle. Nancy, France, 1984"},{"key":"CR44","series-title":"Lect. Notes Comput. Sci.","volume-title":"Proceedings Conference on Rewriting Techniques and Applications, Dijon","author":"H. Zhang","year":"1985","unstructured":"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"}],"container-title":["Acta Informatica"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01178578.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF01178578\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01178578","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,5]],"date-time":"2020-04-05T20:29:10Z","timestamp":1586118550000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF01178578"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1993,2]]},"references-count":44,"journal-issue":{"issue":"2","published-print":{"date-parts":[[1993,2]]}},"alternative-id":["BF01178578"],"URL":"https:\/\/doi.org\/10.1007\/bf01178578","relation":{},"ISSN":["0001-5903","1432-0525"],"issn-type":[{"value":"0001-5903","type":"print"},{"value":"1432-0525","type":"electronic"}],"subject":[],"published":{"date-parts":[[1993,2]]}}}