CoChat
Sign Up
Cited by 579Logic, programming, and type systemsAdvanced Algebra and Logicsemigroups and automata theory

The DOI matches its Crossref record.

Rewrite Systems

DERSHOWITZ, Nachum, JOUANNAUD, Jean-Pierre·1990·Formal Models and Semantics
DOI 10.1016/b978-0-444-88074-1.50011-1
Open this paper in CoChat — free account

Overview

Integrity signals

Registry

Crossref · 10.1016/b978-0-444-88074-1.50011-1

Cites

Statistics

Recomputing p-values needs the paper’s full text.

Verification

Claims the paper makes

We couldn’t retrieve this paper’s full text, so its claims and self-check weren’t run. The registry and citation checks still apply.

Claims other papers make about this one

Each is checked against this paper’s own text: does it say what the citing paper says it does?

Citations

Cites

No references could be resolved yet.

Research works printed but not linked: 199

  1. ANANTHARAMAN, 1990, Identities in alternative rings, J. Automat. Reasoning, 6, 79, 10.1007/BF00302643 · DOI
  2. ARDIS, M.A., Data abstraction transformations, Ph.D. thesis, Report TR-925, Dept. of Computer Science, Univ. of Maryland, August 1980.
  3. BAADER, 1986, Unification in idempotent semigroups is of type zero, J. Automat. Reasoning, 2, 10.1007/BF02328451 · DOI
  4. BACHMAIR, L., Proof by consistency in equational theories, in: Proc. Third IEEE Symposium on Logic in Computer Science, Edinburgh, Scotland (1988) 228–233.
  5. BACHMAIR, L., Proof normalization for resolution and paramodulation, in: Proc. Third International Conference on Rewriting Techniques and Applications, Chapel Hill, NC, Lecture Notes in Computer Science 355 (Springer, Berlin, 1989).
  6. BACHMAIR, L. and N. DERSHOWITZ, Commutation, transformation, and termination, in: Proc. Eighth International Conference on Automated Deduction, Oxford, England, Lecture Notes in Computer Science 230 (Springer, Berlin, 1986) 5–20. · DOI
  7. BACHMAIR, 1989, Completion for rewriting modulo a congruence, Theoret. Comput. Sci., 67, 173, 10.1016/0304-3975(89)90003-0 · DOI
  8. BACHMAIR, L. and N. DERSHOWITZ, Inference rules for rewrite-based first-order theorem proving, in: Proc. Second IEEE Symposium on Logic in Computer Science, Ithaca, NY (1987) 331–337.
  9. BACHMAIR, 1988, Critical pair criteria for completion, J. Symbolic Comput., 6, 1, 10.1016/S0747-7171(88)80018-X · DOI
  10. BACHMAIR, L., N. DERSHOWITZ and J. HSIANG, Orderings for equational proofs, in: Proc. IEEE Symposium on Logic in Computer Science, Cambridge, MA (1986) 346–357.
  11. BACHMAIR, 1985, Associative path ordering, J. Symbolic Comput., 1, 329, 10.1016/S0747-7171(85)80019-5 · DOI
  12. BAETEN, J.C.M., J.A. BERGSTRA and J.W. KLOP, Priority rewrite systems, in: Proc. Second International Conference on Rewriting Techniques and Applications, Bordeaux, France, Lecture Notes in Computer Science 256 (Springer, Berlin, 1987) 83–94. · DOI
  13. BAUDERON, 1987, Graph expressions and graph rewritings, Math. Systems Theory, 20, 83, 10.1007/BF01692060 · DOI
  14. BELLEGARDE, F. and P. LESCANNE, Transformation orderings, in: Proc. Twelfth Colloquium on Trees in Algebra and Programming, Pisa, Italy, Lecture Notes in Computer Science 249 (Springer, Berlin, 1987) 69–80. · DOI
  15. BEN, 1987, Termination of rewriting systems by polynomial interpretations and its implementation, Sci. Comput. Programming, 9, 137, 10.1016/0167-6423(87)90030-X · DOI
  16. BERGSTRA, 1986, Conditional rewrite rules: Confluence and termination, J. Comput. System Sci., 32, 323, 10.1016/0022-0000(86)90033-4 · DOI
  17. BIRKHOFF, 1935, On the structure of abstract algebras, Proc. Cambridge Philos. Soc., 31, 433, 10.1017/S0305004100013463 · DOI
  18. BLEDSOE, 1977, Non-resolution theorem proving, Artificial Intelligence, 9, 1, 10.1016/0004-3702(77)90012-1 · DOI
  19. BOCKMAYR, 1987, A note on a canonical theory with undecidable unification and matching problem, J. Automat. Reasoning, 3, 379, 10.1007/BF00247435 · DOI
  20. BOOK, 1987, Thue systems as rewriting systems, J. Symbolic Comput., 3, 39, 10.1016/S0747-7171(87)80021-4 · DOI
  21. BOOK, 1982, Monadic Thue systems, Theoret. Comput. Sci., 19, 251, 10.1016/0304-3975(82)90036-6 · DOI
  22. BLOOM, 1983, Varieties of “if-then-else”, SIAM J. Comput., 12, 677, 10.1137/0212047 · DOI
  23. BOUDET, 1989, Unification of Boolean rings and Abelian groups, J. Symbolic Comput., 8, 449, 10.1016/S0747-7171(89)80054-9 · DOI
  24. BRAND, D., J.A. DARRINGER and W.J. JOYNER, JR., Completeness of conditional reductions, in: Proc. Fourth Workshop on Automated Deduction, Austin, TX (1979).
  25. BROWN, T.C., JR., A structured design-method for specialized proof procedures, Ph.D. Thesis, California Institute of Technology, Pasadena, CA, 1975.
  26. BUCHBERGER, 1987, History and basic features of the critical-pair/completion procedure, J. Symbolic Comput., 3, 3, 10.1016/S0747-7171(87)80020-2 · DOI
  27. BÜRCKERT, H.-J. J., A. HEROLD and M. SCHMIDT-SCHAUß, On equational theories, unification and decidability, in: Proc. Second International Conference on Rewriting Techniques and Applications, Bordeaux, France, Lecture Notes in Computer Science 256 (Springer, Berlin, 1987) 204–215. · DOI
  28. CHOPPY, C., S. KAPLAN and M. SORIA, Algorithmic complexity of term rewriting systems, in: Proc. Second International Conference on Rewriting Techniques and Applications, Bordeaux, France, Lecture Notes in Computer Science 256 (Springer, Berlin, 1987) 256–285. · DOI
  29. CHURCH, 1936, Some properties of conversion, Trans. Amer. Math. Soc., 39, 472, 10.1090/S0002-9947-1936-1501858-0 · DOI
  30. COLLINS, G., Quantifier elimination for real closed fields by cylindrical algebraic decomposition, in: Proc. Second GI Conference on Automata Theory and Formal Languages, Lecture Notes in Computer Science 33 (Springer, Berlin, 1975) 134–183. · DOI · Paper page
  31. COLMERAUER, A., Equations and inequations on finite and infinite trees, in: Proc. Second International Conference on Fifth Generation Computer Systems, Tokyo, Japan (1984) 85–99.
  32. COMON, 1989, Equational problems and disunification, J. Symbolic Comput., 7, 371, 10.1016/S0747-7171(89)80017-3 · DOI
  33. CUNNINGHAM, 1985, Rewrite systems on a lattice of types, Acta Informat., 22, 149, 10.1007/BF00264228 · DOI
  34. DAUCHET, M., Simulation of Turing machines by a left-linear rewrite rule, in: Proc. Third International Conference on Rewriting Techniques and Applications, Chapel Hill, NC, Lecture Notes in Computer Science 355 (Springer, Berlin, 1989) 109–120. · DOI
  35. DAVIS, 1973, Hilbert's 10th problem, Sci. Amer., 229, 84, 10.1038/scientificamerican1173-84 · DOI
  36. DEHN, 1911, Uber unendliche diskontinuierliche Gruppen, Math. Ann., 71, 116, 10.1007/BF01456932 · DOI
  37. DERSHOWITZ, 1979, A note on simplification orderings, Inform. Process. Lett., 9, 212, 10.1016/0020-0190(79)90071-1 · DOI
  38. DERSHOWITZ, 1982, Orderings for term-rewriting systems, Theoret. Comput. Sci., 17, 279, 10.1016/0304-3975(82)90026-3 · DOI
  39. DERSHOWITZ, N., Applications of the Knuth-Bendix completion procedure, in: Proc. Seminaire d'Informatizue Theorique, Paris, France (1982) 95–111.
  40. DERSHOWITZ, N., Equations as programming language, in: Proc. Fourth Jerusalem Conference on Information Technology (IEEE Computer Society, Silver Spring, MD, 1984) 114–124.
  41. DERSHOWITZ, 1985, Computing with rewrite systems, Inform. and Control, 64, 122, 10.1016/S0019-9958(85)80003-6 · DOI
  42. DERSHOWITZ, 1987, Termination of rewriting, J. Symbolic Comput., 3, 69, 10.1016/S0747-7171(87)80022-6 · DOI
  43. DERSHOWITZ, N., A maximal-literal unit strategy for Horn clauses, in: Proc. Second International Workshop on Conditional and Typed Rewriting Systems, Montreal, Canada, Lecture Notes in Computer Science (Springer, Berlin, to appear).
  44. DERSHOWITZ, 1979, Proving termination with multiset orderings, Comm. AM, 22, 465
  45. DERSHOWITZ, 1988, Existence, uniqueness, and construction of rewrite systems, SIAM J. Comput., 17, 629, 10.1137/0217039 · DOI
  46. DERSHOWITZ, N. and M. OKADA, Proof-theoretic techniques and the theory of rewriting, in: Proc. Third IEEE Symposium on Logic in Computer Science, Edinburgh, Scotland (1988) 104–111.
  47. DERSHOWITZ, 1990, A rationale for conditional equational rewriting, Theoret. Comput. Sci., 75, 111, 10.1016/0304-3975(90)90064-O · DOI
  48. DERSHOWITZ, N., M. OKADA and G. SIVAKUMAR, Confluence of conditional rewrite systems, in: Proc. First International Workshop on Conditional Term Rewriting Systems, Orsay, France, Lecture Notes in Computer Science 308 (Springer, Berlin, 1988) 31–44. · DOI
  49. DERSHOWITZ, N., M. OKADA and G. SIVAKUMAR, Canonical conditional rewrite systems, in: Proc. Ninth Conference on Automated Deduction, Argonne, IL, Lecture Notes in Computer Science 310 (Springer, Berlin, 1988) 538–549. · DOI
  50. DERSHOWITZ, N. and D.A. PLAISTED, Logic programming cum applicative programming, in: Proc. IEEE Symposium on Logic Programming, Boston, MA (1985) 54–66.
  51. DERSHOWITZ, N. and G. SIVAKUMAR, Solving goals in equational languages, in: Proc. First International Workshop on Conditional Term Rewriting Systems, Orsay, France, Lecture Notes in Computer Science 308 (Springer, Berlin, 1988) 45–55. · DOI
  52. DOWNEY, 1980, Variations on the common subexpressions problem, J. Assoc. Computing. Mach., 27, 771, 10.1145/322217.322228 · DOI
  53. EHRENFEUCHT, A., D. HAUSSLER and G. ROZENBERG, On regularity of context-free languages, Theoret. Comput. Sci. 27(3), 311–332. · DOI
  54. EHRIG, H., Introduction to the algebraic theory of graph grammars, in: Proc. International Conference on the Fundamentals of Complexity Theory, Poznán-Kórnik, Poland, Lecture Notes in Computer Science 56 (Springer, Berlin, 1977) 245–255. · DOI
  55. EVANS, 1951, On multiplicative systems defined by generators and relations, I, Proc. Cambridge Philos. Soc., 47, 637, 10.1017/S0305004100027092 · DOI
  56. FAGES, 1987, Associative-commutative unification, J. Symbolic Comput., 3, 257, 10.1016/S0747-7171(87)80004-4 · DOI
  57. FAGES, F. and G. HUET, Unification and matching in equational theories, in: Proc. Eighth Colloquium on Trees in Algebra and Programming, l'Aquilla, Italy, Lecture Notes in Computer Science 159 (Springer, Berlin, 1983) 205–220. · DOI
  58. FAY, M., First-order unification in an equational theory, in: Proc. Fourth Workshop on Automated Deduction, Austin, TX (1979) 161–167.
  59. FEFERMAN, 1968, Systems of predicative analysis II: Representation of ordinals, J. Symbolic Logic, 33, 193, 10.2307/2269866 · DOI
  60. FRIBOURG, 1989, A strong restricton of the inductive completion procedure, J. Symbolic Comput., 8, 253, 10.1016/S0747-7171(89)80069-0 · DOI
  61. FUTATSUGI, K., J.A. GOGUEN, J.-P. JOUANNAUD and J. MESEGUER, Principles of OBJ2, in: Conference Record Twelfth ACM Symposium on Principles of Programming Languages, New Orleans, LA (1985) 52–66.
  62. GALLIER, J.H. and W. SNYDER, A general complete E-unification procedure, in: Proc. Second International Conference on Rewriting Techniques and Applications, Bordeaux, France, Lecture Notes in Computer Science 256 (Springer, Berlin, 1987) 192–203. · DOI
  63. GANZINGER, H., A completion procedure for conditional equations, in: Proc. First International Workshop on Conditional Term Rewriting Systems, Orsay, France, Lecture Notes in Computer Science 308 (Springer, Berlin, 1988) 62–83. · DOI
  64. GARDNER, 1983, Mathematical games: Tasks you cannot help finishing no matter how hard you try to block finishing them, Sci. Amer., 24, 12, 10.1038/scientificamerican0883-12 · DOI
  65. GÖBEL, R., Ground confluence, in: Proc. Second International Conference on Rewriting Techniques and Applications, Bordeaux, France, Lecture Notes in Computer Science 256 (Springer, Berlin, 1987) 156–167. · DOI
  66. GOGUEN, J.A., How to prove algebraic inductive hypotheses without induction, with applications to the correctness of data type implementations, in: Proc. Fifth International Conference on Automated Deduction, Les Arcs, France, Lecture Notes in Computer Science 87 (Springer, Berlin, 1980) 356–373. · DOI
  67. GOGUEN, J.A., J.-P. JOUANNAUD and J. MESEGUER, Operational semantics of order-sorted algebra, in: Proc. Twelfth International EATCS Colloquium on Automata, Languages and Programming, Nafplion, Greece. Lecture Notes in Computer Science 194 (Springer, Berlin, 1985) 221–231. · DOI
  68. GOGUEN, 1985, Completeness of many sorted equational deduction, Houston J. Math., 11, 307
  69. GOGUEN, J.A. and J.J. TARDO, An introduction to OBJ: A language for writing and testing formal algebraic specifications, in: Proc. Specification of Reliable Software Conference (1979) 170–189.
  70. GOLDFARB, 1981, Note on the undecidability of the second-order unification problem, Theoret. Comput. Sci., 13, 225, 10.1016/0304-3975(81)90040-2 · DOI
  71. GUESSARIAN, 1987, On the axiomatization of “if-then-else”, SIAM J. Comput., 16, 332, 10.1137/0216025 · DOI
  72. GUTTAG, 1977, Abstract data types and the development of data structures, Comm. ACM, 20, 396, 10.1145/359605.359618 · DOI
  73. HEILBRUNNER, 1987, The undecidability of the unification and matching problem for canonical theories, Acta Informat., 24, 157, 10.1007/BF00264362 · DOI
  74. HENKIN, 1977, The logic of equality, Amer. Math. Monthly, 84, 597, 10.2307/2321009 · DOI
  75. HEROLD, 1987, Unification in Abelian semi-groups, J. Automat. Reasoning, 3, 247, 10.1007/BF00243791 · DOI
  76. HIGMAN, G., Ordering by divisibility in abstract algebras, Proc. London Math. Soc. (3) 2(7) (1952) 326–336. · DOI · Paper page
  77. HIGMAN, 1952, Groups as groupoids with one law, Publ. Math. Debrecen, 2, 215, 10.5486/PMD.1952.2.3-4.10 · DOI
  78. HINDLEY, J.R., The Church-Rosser property and a result in combinatory logic, Ph.D. Thesis, Univ. of Newcastle-upon-Tyne, 1964.
  79. HOFFMANN, C.M. and M.J. O'DONNELL, Interpreter generation using tree pattern matching, in: Conf. Rec. Sixth ACM Symposium on Principles of Programming Languages, San Antonio, TX (1979) 169–179. · DOI
  80. HSIANG, J., Topics in automated theorem proving and program generation, Ph.D. Thesis, Report R-82–1113, Dept. of Computer Science, Univ. of Illinois, Urbana, IL, 1982.
  81. HSIANG, 1985, Refutational theorem proving using term-rewriting systems, Artificial Intelligence, 25, 255, 10.1016/0004-3702(85)90074-8 · DOI
  82. HSIANG, J. and N. DERSHOWITZ, Rewrite methods for clausal and non-clausal theorem proving, in: Proc. Tenth International Colloquium on Automata, Languages and Programming, Barcelona, Spain, Lecture Notes in Computer Science 154 (Springer, Berlin, 1983) 331–346. · DOI
  83. HSIANG, J. and J.-P. JOUANNAUD, Complete sets of inference rules for E-unification, in: Proc. Second Unification Workshop, Val d'Ajol, France (1988); available as: CRIN Report, Univ. de Nancy, France.
  84. HSIANG, J. and M. RUSINOWITCH, A new method for establishing refutational completeness in theorem proving, in: Proc. Eight International Conference on Automated Deduction, Oxford, England, Lecture Notes in Computer Science 230 (Springer, Berlin, 1986) 141–152. · DOI
  85. HSIANG, J. and M. RUSINOWITCH, On word problems in equational theories, in: Proc. Fourteenth International Colloquium on Automata, Languages and Programming, Karlsruhe, West Germany, Lecture Notes in Computer Science 267 (Springer, Berlin, 1987) 54–71. · DOI
  86. HUET, 1980, Confluent reductions: Abstract properties and applications to term rewriting systems, J. Assoc. Comput. Mach., 27, 797, 10.1145/322217.322230 · DOI
  87. HUET, 1981, A complete proof of correctness of the Knuth-Bendix completion algorithm, J. Comput. System Sci., 23, 11, 10.1016/0022-0000(81)90002-7 · DOI
  88. HUET, G., Cartesian closed categories and lambda-calculus, in: Proc. Spring School on Combinators and Functional Programming Languages, Val d'Ajol, France, Lecture Notes in Computer Science (Springer, Berlin) 123–135. · DOI
  89. HUET, G. and J.-M. HULLOT, Proofs by induction in equational theories with constructors, in: Proc. Twenty-First IEEE Symposium on Foundations of Computer Science, Lake Placid, NY (1980) 96–107.
  90. HUET, G. and J.-J. LÉVY, Call by need computations in non-ambiguous linear term rewriting systems, in: J. Lassez and G. Plotkin, eds., Computational Logic: Essays in Honour of Alan Robinson (MIT Press, Cambridge, MA, to appear).
  91. HULLOT, J.-M., Canonical forms and unification, in: Proc. Fifth International Conference on Automated Deduction, Les Arcs, France, Lecture Notes in Computer Science 87 (Springer, Berlin, 1980) 318–334. · DOI
  92. ITURRIAGA, R., Contributions to mechanical mathematics, Ph.D. Thesis, Dept. of Computer Science, Carnegie-Mellon Univ., Pittsburgh, PA, 1967.
  93. JOUANNAUD, J.-P., Confluent and coherent sets of reductions with equations: Application to proofs in abstract data types, in: Proc. Eighth Colloquium on Trees in Algebra and Programming, Lecture Notes in Computer Science 59 (Springer, Berlin, 1983) 269–283. · DOI
  94. JOUANNAUD, J.-P., C. KIRCHNER and H. KIRCHNER, Incremental construction of unification algorithms in equational theories, in: Proc. Tenth International Colloquium on Automata, Languages and Programming, Barcelona, Spain, Lecture Notes in Computer Science 154 (Springer, Berlin, 1983) 361–373. · DOI
  95. JOUANNAUD, 1986, Completion of a set of rules modulo a set of equations, SIAM J. Comput., 15, 1155, 10.1137/0215084 · DOI
  96. JOUANNAUD, 1989, Automatic proofs by induction in equational theories without constructors, Inform. and Comput., 82, 1, 10.1016/0890-5401(89)90062-X · DOI
  97. JOUANNAUD, 1987, Rewriting systems, Tech. Sci. Inform., 6, 181
  98. JOUANNAUD, J.-P. and M. MUÑOZ, Termination of a set of rules modulo a set of equations, in: Proc. Seventh International Conference on Automated Deduction, Napa, CA, Lecture Notes in Computer Science 170 (Springer, Berlin, 1984) 175–193. · DOI
  99. JOUANNAUD, J.-P. and B. WALDMANN, Reductive conditional term rewriting systems, in: Proc. Third IFIP Working Conference on Formal Description of Programming Concepts, Ebberup, Denmark (1986).
  100. KAPLAN, 1987, Simplifying conditional term rewriting systems: Unification, termination and confluence, J. Symbolic Comput., 4, 295, 10.1016/S0747-7171(87)80010-X · DOI
  101. KAPUR, 1987, Proof by consistency, Artificial Intelligence, 31, 125, 10.1016/0004-3702(87)90017-8 · DOI
  102. KAPUR, 1988, Only prime superpositions need be considered for the Knuth-Bendix procedure, J. Symbolic Comput., 4, 19, 10.1016/S0747-7171(88)80019-1 · DOI
  103. KAPUR, D. and P. NARENDRAN, An equational approach to theorem proving in first-order predicate calculus, in: Proc. Ninth International Joint Conference on Artificial Intelligence, Los Angeles, CA (1985) 1146–1153.
  104. KAPUR, D. and P. NARENDRAN, NP-completeness of set unification and matching problems, in: Proc. Eighth International Conference on Automated Deduction, Oxford, England, Lecture Notes in Computer Science 230 (Springer, Berlin, 1986) 489–495. · DOI
  105. KAPUR, 1987, Matching, unification and complexity (A preliminary note), SIGSAM Bull., 21, 6, 10.1145/36330.36332 · DOI
  106. KAPUR, D., P. NARENDRAN and H. ZHANG, Proof by induction using test sets, in: Proc. Eighth International Conference on Automated Deduction, Oxford, England, Lecture Notes in Computer Science 230 (Springer-Verlag, Berlin, 1986) 99–117. · DOI
  107. KAPUR, 1989, On ground confluence of term rewriting systems, Inform. Comput., 86, 14, 10.1016/0890-5401(90)90023-B · DOI
  108. KAPUR, 1987, On sufficient completeness and related properties of term rewriting systems, Acta Informat., 24, 395, 10.1007/BF00292110 · DOI
  109. KAPUR, D. and H. ZHANG, An overview of Rewrite Rule Laboratory (RRL), in: Proc. Third International Conference on Rewriting Techniques and Applications, Chapel Hill, NC, Lecture Notes in Computer Science 355 (Springer, Berlin, 1989) 559–563. · DOI
  110. KIRBY, 1982, Accessible independence results for Peano arithmetic, Bull. London Math. Soc., 14, 285, 10.1112/blms/14.4.285 · DOI
  111. KIRCHNER, C., Computing unification algorithms, in: Proc. First IEEE Symposium on Logic in Computer Science, Cambridge, MA. (1986) 206–216.
  112. KLOP, 1987, Term rewriting systems: A tutorial, Bull. European Assoc. Theoret. Comput. Sci., 32, 143
  113. KNIGHT, 1989, Unification: A multidisciplinary survey, Comput. Surveys, 21, 93, 10.1145/62029.62030 · DOI
  114. KOUNALIS, E., Completeness in data type specifications, in: Proc. EUROCAL Conference, Linz, Austria (1985).
  115. KOUNALIS, E. and M. RUSINOWITCH, On word problems in Horn theories, in: Proc. Ninth International Conference on Automated Deduction, Argonne, IL, Lecture Notes in Computer Science 310 (Springer-Verlag, Berlin, 1988) 527–537. · DOI
  116. KRUSKAL, 1960, Well-quasi-ordering, the Tree Theorem, and Vazsonyi's conjecture, Trans. Amer. Math. Society, 95, 210
  117. KRUSKAL, 1972, The theory of well-quasi-ordering: A frequently discovered concept, J. Combin. Theory Ser. A, 13, 297, 10.1016/0097-3165(72)90063-5 · DOI
  118. LANKFORD, D.S. and A.M. BALLANTYNE, The refutation completeness of blocked permutative narrowing and resolution, in: Proc. Fourth Workshop on Automated Deduction, Austin, TX (1979) 53–59.
  119. LAUTEMANN, 1988, A note on polynomial interpretation, Bull. European Assoc. Theoret. Comput. Sci., 36, 129
  120. LE CHENADEC, 1987, Analysis of Dehn's algorithm by critical pairs, Theoret. Comput. Sci., 51, 27, 10.1016/0304-3975(87)90048-X · DOI
  121. LESCANNE, P., Computer experiments with the REVE term rewriting system generator, in: Proc. Tenth ACM Symposium on Principles of Programming Languages, Austin, TX (1983) 99–108.
  122. LESCANNE, P., Uniform termination of term-rewriting systems with status, in: Proc. Ninth Colloquium on Trees in Algebra and Programming (Cambridge University Press, Cambridge, 1984).
  123. LOOS, R., Term reduction systems and algebraic algorithms, in: Proc. Fifth GI Workshop on Artificial Intelligence, Bad Honnef, West Germany, Informatik Fachberichte (Springer, Berlin, 1981) 214–234. · DOI
  124. MAHER, M.J., Complete axiomatizations of the algebras of the finite, rational and infinite trees, in: Proc. Third IEEE Symposium on Logic in Computer Science, Edinburgh, Scotland (1988) 348–357.
  125. MAKANIN, 1977, The problem of solvability of equations in a free semi-group, Akad. Nauk SSSR, 233
  126. MANNA, Z. and S. NESS, On the termination of Markov algorithms, in: Proc. Third Hawaii International Conference on System Science, Honolulu, HI (1970) 789–792.
  127. MARKOV, 1947, The impossibility of some algorithms in the theory of associative systems, Dokl. Akad. Nauk SSSR, 55, 587
  128. MARTELLI, 1982, An efficient unification algorithm, ACM Trans. Programm. Languages and Systems, 4, 258, 10.1145/357162.357169 · DOI
  129. MARTIN, U., How to choose the weights in the Knuth-Bendix ordering, in: Proc. Second International Conference on Rewriting Techniques and Applications, Bordeaux, France, Lecture Notes in Computer Science 256 (Springer, Berlin, 1987) 42–53. · DOI
  130. MATIJASEVIC, 1967, Simple examples of undecidable associative calculi, Soviet Math. (Dokl.), 8, 555
  131. MATIJASEVIC, 1970, Enumerable sets are Diophantine, Soviet Math. (Dokl.), 11, 354
  132. MCNULTY, G.F., An equational logic sampler, in: Proc. Third International Conference on Rewriting Techniques and Applications, Chapel Hill, NC, Lecture Notes in Computer Science 355 (Springer, Berlin, 1989) 234–262. · DOI
  133. MESEGUER, 1989, Order-sorted unification, J. Symbolic Comput., 8, 383, 10.1016/S0747-7171(89)80036-7 · DOI
  134. METIVIER, 1983, About the rewriting systems produced by the Knuth-Bendix completion algorithm, Inform. Process. Lett., 16, 31, 10.1016/0020-0190(83)90009-1 · DOI
  135. MUSSER, D.R., On proving inductive properties of abstract data types, in: Proc. Seventh ACM Symposium on Principles of Programming Languages, Las Vegas, NV (1980) 154–162.
  136. NASH-WILLIAMS, C. ST. J.A., On well-quasi-ordering finite trees, Proc. Cambridge Philos. Soc. 59(4) (1963) 833–835. · DOI
  137. NEWMAN, 1942, On theories with a combinatorial definition of ‘equivalence’, Ann. Math., 43, 223, 10.2307/1968867 · DOI
  138. NIPKOW, T. and G. WEIKUM, A decidability result about sufficient-completeness of axiomatically specified abstract data types, in: Proc. Sixth GI Conference on Theoretical Computer Science, Lecture Notes in Computer Science 145 (Springer, Berlin, 1982) 257–268. · DOI
  139. NUTT, 1989, Basic narrowing revisited, J. Symbolic Comput., 7, 295, 10.1016/S0747-7171(89)80014-8 · DOI
  140. O'DONNELL, M.J., Subtree replacement systems: A unifying theory for recursive equations, LISP, Lucid and Combinatory Logic, in: Proc. Ninth ACM Symposium on Theory of Computing (1977) 295–305.
  141. OYAMAGUCHI, 1987, The Church-Rosser property for ground term rewriting systems is decidable, Theoret. Comput. Sci., 49, 43, 10.1016/0304-3975(87)90100-9 · DOI
  142. PATERSON, 1978, Linear unification, J. Comput. System Sci., 16, 158, 10.1016/0022-0000(78)90043-0 · DOI
  143. PEDERSEN, J., Morphocompletion for one-relation monoids, in: Proc. Third International Conference on Rewriting Techniques and Applications, Chapel Hill, NC, Lecture Notes in Computer Science 355 (Springer, Berlin, 1989).
  144. PETERSON, 1983, A technique for establishing completeness results in theorem proving with equality, SIAM J. Comput., 12, 82, 10.1137/0212006 · DOI
  145. PETERSON, 1981, Complete sets of reductions for some equational theories, J. Assoc. Comput. Mach., 28, 233, 10.1145/322248.322251 · DOI
  146. PLAISTED, 1985, Semantic confluence tests and completion methods, Inform. and Control, 65, 182, 10.1016/S0019-9958(85)80005-X · DOI
  147. POST, 1947, Recursive unsolvability of a problem of Thue, J. Symbolic Logic, 13, 1, 10.2307/2267170 · DOI
  148. PUEL, 1989, Using unavoidable sets of trees to generalize Kruskal's theorem, J. Symbolic Comput., 8, 335, 10.1016/S0747-7171(89)80035-5 · DOI
  149. PUEL, L., Embedding with patterns and associated recursive ordering, in: Proc. Third International Conference on Rewriting Techniques and Applications, Chapel Hill, NC, Lecture Notes in Computer Science 355 (Springer, Berlin, 1989) 371–387. · DOI
  150. RAOULT, 1981, Finiteness results on rewriting systems, R.A.I.R.O. Theoret. Inform., 15, 373
  151. RAOULT, 1984, On graph rewritings, Theoret. Comput. Sci., 32, 1, 10.1016/0304-3975(84)90021-5 · DOI
  152. RAOULT, 1980, Operational and semantic equivalence between recursive programs, J. Assoc. Comput. Mach., 27, 772, 10.1145/322217.322229 · DOI
  153. ROBINSON, 1965, A machine-oriented logic based on the resolution principle, J. Assoc. Comput. Mach., 12, 23, 10.1145/321250.321253 · DOI
  154. ROSEN, 1973, Tree-manipulating systems and Church-Rosser theorems, J. Assoc. Comput. Mach., 20, 160, 10.1145/321738.321750 · DOI
  155. RUSINOWITCH, 1987, Path of subterms ordering and recursive decomposition ordering revisited, J. Symbolic Comput., 3
  156. SCHMIDT-SCHAUß, M. Unification in a combination of arbitrary disjoint equational theories, in: Proc. Ninth International Conference on Automated Deduction, Argonne, IL, Lecture Notes in Computer Science 310 (Springer, Berlin, 1988) 378–396. · DOI
  157. SETHI, 1974, Testing for the Church-Rosser property, J. Assoc. Comput. Mach., 21, 671, 10.1145/321850.321862 · DOI
  158. SHOSTAK, 1979, An efficient decision procedure for arithmetic with function symbols, J. Assoc. Comput. Mach., 26, 351, 10.1145/322123.322137 · DOI
  159. SIEKMANN, J., Universal unification, in: Proc. Seventh International Conference on Automated Deduction, Napa, CA, Lecture Notes in Computer Science 170 (Springer, Berlin, 1984) 1–42. · DOI
  160. SNYDER, W., Efficient ground completion: An O(n log n) algorithm for generating reduced sets of ground rewrite rules equivalent to a set of ground equations E Proc. Third International Conference on Rewriting Techniques and Applications, Chapel Hill, NC, Lecture Notes in Computer Science 355 (Springer, Berlin, 1989) 419–433. · DOI
  161. STICKEL, 1981, A unification algorithm for associative-commutative functions, J. Assoc. Comput. Mach., 28, 423, 10.1145/322261.322262 · DOI
  162. STICKEL, M.E., The KLAUS automated deduction system, in: Proc. Eighth International Conference on Automated Deduction, Oxford, England, Lecture Notes in Computer Science 230 (Springer, Berlin, 1986) 703–704. · DOI
  163. STONE, 1936, The theory of representations for Boolean algebra, Trans. Amer. Math. Soc., 40, 37
  164. SZABO, P., Unifikationstheorie erster Ordnung, Thesis, Fakultät für Informatik, Univ. Karlsruhe, Karlsruhe, West Germany, 1982.
  165. THIEL, J.J., Stop losing sleep over incomplete data type specifications, in: Conf. Rec. ACM Symposium on Principles of Programming Languages, Salt Lake City, UT (1984) 76–82.
  166. THUE, 1914, Probleme über Veranderungen von Zeichenreihen nach gegeben Regeln, Skr. Vid. Kristianaia I. Mat. Naturv. Klasse, 10/34
  167. TOYAMA, 1987, On the Church-Rosser property for the direct sum of term rewriting systems, J. Assoc. Comput. Mach., 34, 128, 10.1145/7531.7534 · DOI
  168. TOYAMA, 1987, Counterexamples to termination for the direct sum of term rewriting systems, Inform. Process. Lett., 25, 141, 10.1016/0020-0190(87)90122-0 · DOI
  169. TOYAMA, Y., J.W. KLOP and H.P. BARENDREGT, Termination for the direct sum of left-linear term rewriting systems, in: Proc. Third International Conference on Rewriting Techniques and Applications, Chapel Hill, NC, Lecture Notes in Computer Science 355 (Springer, Berlin, 1989) 477–491. · DOI
  170. WALTHER, 1988, Many-sorted unification, J. Assoc. Comput. Mach., 35, 1, 10.1145/42267.45071 · DOI
  171. WINKLER, F. and B. BUCHBERGER, A criterion for eliminating unnecessary reductions in the Knuth-Bendix algorithm, in: Proc. Colloquium on Algebra, Combinatorics and Logic in Computer Science, Györ, Hungary (1983).
  172. YELICK, 1987, Unification in combinations of collapse-free regular theories, J. Symbolic Comput., 3, 153, 10.1016/S0747-7171(87)80025-1 · DOI
  173. ZHANG, H., Reduction, superposition & induction: automated reasoning in an equational logic, Ph.D. Thesis, Rensselaer Polytechnic Institute, Troy, NY, 1988.
  174. ZHEGALKIN, 1927, On a technique of evaluation of propositions in symbolic logic, Mat. Sb., 34, 9
  175. BACHMAIR, L. and H. GANZINGER, On restrictions of ordered paramodulation with simplification, in: Proc. Second International Workshop on Conditional and Typed Rewriting Systems, Montreal, Canada, Lecture Notes in Computer Science (Springer, Berlin, to appear).
  176. BERTLING, H. and H. GANZINGER, Completion-time optimization of rewrite-time goal solving, in: Proc. Third International Conference on Rewriting Techniques and Applications, Chapel Hill, NC, Lecture Notes in Computer Science 355 (Springer, Berlin, 1989) 45–58. · DOI
  177. BOOK, 1982, Confluent and other types of Thue systems, J. Assoc. Comput. Machin., 29, 171, 10.1145/322290.322301 · DOI
  178. CHEW, P., An improved algorithm for computing with equations, in: Proc. Twenty-First IEEE Symposium on Foundations of Computer Science, Lake Placid, NY (1980) 108–117.
  179. COMON, H., Disunification: A survey, in: J. Lassez and G. Plotkin, eds., Computational Logic: Essays in Honour of Alan Robinson (MIT Press, Cambridge, MA, to appear).
  180. DERSHOWITZ, 1990, Notations for rewriting, Bull. European Assoc. Theoret. Comput. Sci.
  181. GALLIER, 1989, Complete sets of transformations for general E-Unification, Theoret. Comput. Sci., 67, 203, 10.1016/0304-3975(89)90004-2 · DOI
  182. GALLIER, J. and W. SNYDER, Designing unification procedures using transformations: A survey, in: Proc. Workshop on Logic from Computer Science, Berkeley, CA (1990).
  183. GESER, A., Termination Relative, Doctoral Dissertation, Univ. Passau, Passau, 1989.
  184. GNAEDIG, I., C. KIRCHNER and H. KIRCHNER, Equational completion in order-sorted agebras, in: Proc. Thirteenth Colloquium on Trees in Algebra and Programming, Nancy, France (1988) 165–184.
  185. HALPERN, 1990, Completeness of rewrite rules and rewrite strategies for FP, J. Assoc. Comput. Mach., 37, 86, 10.1145/78935.78939 · DOI
  186. HUET, G. and J.-J. LÉVY, Computations in orthogonal term rewriting systems, in: J. Lassez and G. Plotkin, eds., Computational Logic: Essays in Honour of Alan Robinson (MIT Press, Cambridge, MA, to appear).
  187. JAFFAR, 1990, Minimal and complete word unification, J. Assoc. Comput. Mach., 37, 47, 10.1145/78935.78938 · DOI
  188. JOUANNAUD, J. and C. KIRCHNER, Solving equations in abstract algebras: A rule-based survey of unification, in: J. Lassez and G. Plotkin, eds., Computational Logic: Essays in Honour of Alan Robinson (MIT Press, Cambridge, MA, to appear).
  189. KAPUR, D. and D.R. MUSSER, Inductive reasoning for incomplete specifications, in: Proc. IEEE Symposium on Logic in Computer Science, Cambridge, MA (1986) 367–377.
  190. KÜCHLIN, W., A confluence criterion based on the generalized Newman lemma, in: Proc. EUROCAL Conference, Linz, Austria (1985).
  191. LANKFORD, D., G. BUTLER and A. BALLANTYNE, A progress report on new decision algorithms for finitely presented Abelian groups, in: Proc. Seventh International Conference on Automated Deduction, Napa, CA, Lecture Notes in Computer Science 170 (Springer, Berlin, 1984) 128–141. · DOI
  192. MARTIN, 1989, A geometrical approach to multiset orderings, Theoret. Comput. Sci., 67, 37, 10.1016/0304-3975(89)90020-0 · DOI
  193. MIDDELDORP, A., Modular aspects of properties of term rewriting systems related to normal forms, in: Proc. Third International Conference on Rewriting Techniques and Applications, Chapel Hill, NC, Lecture Notes in Computer Science 355 (Springer, Berlin, 1989) 263–277. · DOI
  194. PAUL, 1985, Equational methods in first order predicate calculus, J. Symbolic Comput., 1, 7, 10.1016/S0747-7171(85)80026-2 · DOI
  195. RUŽIČKA, 1989, An almost linear Robinson unification algorithm, Acta Informat., 27, 61, 10.1007/BF00263501 · DOI
  196. SEKAR, R.C. and I.V. RAMAKRISHNAN, Programming in equational logic: Beyond strong sequentiality, in: Proc. Fifth IEEE Symposium on Logic in Computer Science, Philadelphia, PA (1990).
  197. SLAGLE, 1974, Automated theorem-proving for theories with simplifiers, commutativity, and associativity, J. Assoc. Comput. Mach., 21, 622, 10.1145/321850.321859 · DOI
  198. ZHANG, H. and D. KAPUR, First-order theorem proving using conditional equations, in: Proc. Ninth International Conference on Automated Deduction, Argonne, IL, Lecture Notes in Computer Science 310 (Springer, Berlin, 1988) 1–20. · DOI
  199. SMOLKA, G., Logic programming over polymorphically order-sorted types, Ph.D. Thesis, Univ. Kaiserslautern. 1989. · DOI

Cited by

Sorted by citations

See all 579

Metadata

Authors
DERSHOWITZ, N., & JOUANNAUD, J.-P.
Affiliations
  • University of Illinois Urbana-Champaign (US)
  • Université Paris-Sud (FR)
ORCID
Venue
Formal Models and Semantics
Publisher
Elsevier
Published
1990
Pages
243-320
DOI
10.1016/b978-0-444-88074-1.50011-1
OpenAlex
W3022794709
Cited by
579
References
0
Citations by year
2026: 5 · 2025: 6 · 2024: 8 · 2023: 2 · 2022: 5 · 2021: 4 · 2020: 8 · 2019: 7 · 2018: 3 · 2017: 11 · 2016: 3 · 2015: 5 · 2014: 5 · 2013: 3 · 2012: 8
FWCI
42.18
Type
book chapter
Language
en
Open access
closed
Licence
www.elsevier.com/tdm/userlicense/1.0/ (tdm)
Locations
Elsevier eBooks (publishedVersion)
Topics
  • Physical Sciences › Computer Science › Software › Logic, programming, and type systems
  • Physical Sciences › Computer Science › Computational Theory and Mathematics › Advanced Algebra and Logic
  • Physical Sciences › Computer Science › Computational Theory and Mathematics › semigroups and automata theory
Keywords
rewrite systems, term rewriting, normal forms, termination proofs, convergence, decision procedures, lambda calculus, combinatory logic, binary relations, equational logic

About these checks

Registry, retraction, Cites and statistics results are computed, not judged, with one exception: a printed reference that no index lists is read once by a model before it counts as a citation error. Claims are extracted by a model and kept only when their quote appears verbatim in the text; each cited source is then checked, with a model’s help, for whether it says what the claim relies on. Those verdicts can be wrong — read the claim’s quote and the cited source before relying on one.

Statistics and arithmetic are recomputed, not judged.

Confidence bands are shown only for fields calibrated on our annotated test set. None is calibrated yet, so no band is shown.

What counts as a claim ›How we measure confidence ›How we check this ›

Are you an author, or do you see a problem with this page? Request a review