ACM Portal
  Subscribe (Full Service)    Register (Limited Service, Free)    Login
  Search:   The ACM Digital Library   The Guide
  
ACM Home Page
Please provide us with feedback. Feedback
Completion of a set of rules modulo a set of equations
Full text PdfPdf (660 KB)
Source Annual Symposium on Principles of Programming Languages archive
Proceedings of the 11th ACM SIGACT-SIGPLAN symposium on Principles of programming languages table of contents
Salt Lake City, Utah, United States
Pages: 83 - 92  
Year of Publication: 1984
ISBN:0-89791-125-3
Authors
Jean-Pierre Jouannaud  CRIN, BP 239, 54506 Vandoeuvre les Nancy, CEDEX (FRENCE)
Helene Kirchner  CRIN, BP 239, 54506 Vandoeuvre les Nancy, CEDEX (FRENCE)
Sponsors
SIGACT: ACM Special Interest Group on Algorithms and Computation Theory
SIGADA: ACM Special Interest Group on Ada Programming Language
SIGAPL: ACM Special Interest Group on APL Programming Language
Publisher
ACM  New York, NY, USA
Bibliometrics
Downloads (6 Weeks): 3,   Downloads (12 Months): 36,   Citation Count: 2
Additional Information:

references   cited by   index terms   collaborative colleagues  

Tools and Actions: Request Permissions Request Permissions    Review this Article  
DOI Bookmark: Use this link to bookmark this Article: http://doi.acm.org/10.1145/800017.800519
What is a DOI?

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

 
1
DERANSART P.: private communication
 
2
DERSHOWITZ N.: "Computing with term rewriting systems" to be published
 
3
GOGUEN J.A., MESEGUER J., PLAISTED D.: "Programming with parameterized abstract objects in OBJ" in "Theory and Practice of Software Technology", Ferrari D., Bolognani M. and Goguen J.A. Eds., North Holland (1982).
 
4
Jieh Hsiang , Nachum Dershowitz, Rewrite Methods for Clausal and Non-Clausal Theorem Proving, Proceedings of the 10th Colloquium on Automata, Languages and Programming, p.331-346, July 18-22, 1983
 
5
HUET G. HULLOT. J.M.: "Proofs by induction in equational theories with constructors" Proc. 21th FOGS (l980).
6
Gérard Huet, Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems: Abstract Properties and Applications to Term Rewriting Systems, Journal of the ACM (JACM), v.27 n.4, p.797-821, Oct. 1980  [doi>10.1145/322217.322230]
 
7
HUET G.: "A complete proof of correctness of the Knuth and Bendix completion algorithm" TCSS 23, pp 11-21 (19,81).
 
8
Jean-Pierre Jouannaud, Confluent and Coherent Equational Term Rewriting Systems: Application to Proofs in Abstract Data Types, Proceedings of the 8th Colloquium on Trees in Algebra and Programming, p.269-283, March 09-11, 1983
 
9
Jean-Pierre Jouannaud , Claude Kirchner , Hélène Kirchner, Incremental Construction of Unification Algorithms in Equational Theories, Proceedings of the 10th Colloquium on Automata, Languages and Programming, p.361-373, July 18-22, 1983
 
10
JOUANNAUD J. P. LESCANNE. P.: "On nultiset ordering" IPL 10-2, pp57-63.
 
11
KNUTH D. BENDTY P.: "Simple word problems in universal algebras" in "Computational problems in abstract algebra" Leech J. ed. Pergamon Press, pp 263-297 (1970)
 
12
LANKFORD D.S., BALLANTYNE. A.M.: ";Decision procedures for simple equationnal theories with permutative axioms: complete sets of permutative reductions." Rep. ATP-37, Dpt. of Comp. Sc., Univ. of Texas at Austin.
13
Pierre Lescanne, Computer experiments with the REVE term rewriting system generator, Proceedings of the 10th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.99-108, January 24-26, 1983, Austin, Texas  [doi>10.1145/567067.567078]
14
Gerald E. Peterson , Mark E. Stickel, Complete Sets of Reductions for Some Equational Theories, Journal of the ACM (JACM), v.28 n.2, p.233-264, April 1981  [doi>10.1145/322248.322251]

CITED BY  2
Wray L. Buntine , Hans-Jürgen Bürckert, On solving equations and disequations, Journal of the ACM (JACM), v.41 n.4, p.591-629, July 1994
Kokichi Futatsugi , Joseph A. Goguen , Jean-Pierre Jouannaud , José Meseguer, Principles of OBJ2, Proceedings of the 12th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.52-66, January 14-16, 1985, New Orleans, Louisiana, United States

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.2 Grammars and Other Rewriting Systems
          Subjects: Parallel rewriting systems (e.g., developmental systems, L-systems)

Additional Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Proof theory


General Terms:
Languages, Theory, Verification

Collaborative Colleagues:
Jean-Pierre Jouannaud: colleagues
Helene Kirchner: colleagues

The ACM Portal is published by the Association for Computing Machinery. Copyright © 2009 ACM, Inc.
Terms of Usage   Privacy Policy   Code of Ethics   Contact Us

Useful downloads: Adobe Acrobat    QuickTime    Windows Media Player    Real Player