Skip to main content
SpringerLink
Log in
Book cover

Algebra, Meaning, and Computation pp 497–520Cite as

Completion Is an Instance of Abstract Canonical System Inference

  • Chapter

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 4060))

Abstract

Abstract canonical systems and inference (ACSI) were introduced to formalize the intuitive notions of good proof and good inference appearing typically in first-order logic or in Knuth-Bendix like completion procedures.

Since this abstract framework is intended to be generic, it is of fundamental interest to show its adequacy to represent the main systems of interest. This has been done for ground completion (where all equational axioms are ground) but was still an open question for the general completion process.

By showing that the standard completion is an instance of the ACSI framework we close the question. For this purpose, two proof representations, proof terms and proofs by replacement, are compared to built a proof ordering that provides an instantiation adapted to the abstract canonical system framework.

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

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Aiguier, M., Bahrami, D.: Structures for abstract rewriting. Journal of Automated Reasoning (2006) (to appear)

    Google Scholar 

  2. Baader, F., Nipkow, T.: Term Rewriting and all That. Cambridge University Press, Cambridge (1998)

    Google Scholar 

  3. Bachmair, L.: Proof methods for equational theories. PhD thesis, University of Illinois, Urbana-Champaign (Ill. USA) (1987), Revised version (August 1988)

    Google Scholar 

  4. Bachmair, L., Dershowitz, N.: Equational inference, canonical proofs, and proof orderings. Journal of Association for Computing Machinery 41(2), 236–276 (1994)

    MATH  MathSciNet  Google Scholar 

  5. Bachmair, L., Ganzinger, H.: Resolution theorem proving. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. 1, ch. 2, pp. 19–99. Elsevier Science, Amsterdam (2001)

    Chapter  Google Scholar 

  6. Bonacina, M.P., Dershowitz, N.: Abstract Canonical Inference. ACM Transactions on Computational Logic (2006) (to appear)

    Google Scholar 

  7. Bonacina, M.P., Hsiang, J.: On rewrite programs: semantics and relationship with Prolog. Journal of Logic Programming 14(1-2), 155–180 (1992)

    Article  MATH  MathSciNet  Google Scholar 

  8. Borovansky, P., Kirchner, C., Kirchner, H., Moreau, P.-E.: ELAN from a rewriting logic point of view. Theoretical Computer Science 2(285), 155–185 (2002)

    Article  MathSciNet  Google Scholar 

  9. Buchberger, B.: An algorithm for finding a basis for the residue class ring of a zero-dimensional polynomial ideal. PhD thesis, University of Inssbruck (Austria) (1965) (in German)

    Google Scholar 

  10. Buchberger, B.: A critical-pair/completion algorithm for finitely generated ideals in rings. In: Börger, E., Rödding, D., Hasenjaeger, G. (eds.) Rekursive Kombinatorik 1983. LNCS, vol. 171, pp. 137–161. Springer, Heidelberg (1984)

    Google Scholar 

  11. Bündgen, R.: Simulating Buchberger‘s algorithm by Knuth-Bendix completion. In: Book, R.V. (ed.) RTA 1991. LNCS, vol. 488, pp. 386–397. Springer, Heidelberg (1991)

    Google Scholar 

  12. Burel, G.: Systèmes Canoniques Abstraits: Application à la Déduction Naturelle et à la Complétion. Master’s thesis, Université Denis Diderot – Paris 7 (2005)

    Google Scholar 

  13. Cirstea, H., Kirchner, C.: The rewriting calculus — Part I and II. Logic Journal of the Interest Group in Pure and Applied Logics 9(3), 427–498 (2001)

    MathSciNet  Google Scholar 

  14. Clavel, M., Eker, S., Lincoln, P., Meseguer, J.: Principles of Maude. In: Meseguer, J. (ed.) Proceedings of the first international workshop on rewriting logic, Asilomar, California, September 1996. Electronic Notes in Theoretical Computer Science, vol. 4 (1996)

    Google Scholar 

  15. Dershowitz, N.: Computing with rewrite systems. Information and Control 65(2-3), 122–157 (1985)

    Article  MATH  MathSciNet  Google Scholar 

  16. Dershowitz, N.: Canonicity. Electronic Notes in Theoretical Computer Science 86(1) (2003)

    Google Scholar 

  17. Dershowitz, N., Kirchner, C.: Abstract saturation-based inference. In: Kolaitis, P. (ed.) Proceedings of LICS 2003, Ottawa, Ontario (June 2003) ieee

    Google Scholar 

  18. Dershowitz, N., Kirchner, C.: Abstract Canonical Presentations. Theorical Computer Science (2006) (to appear)

    Google Scholar 

  19. Dowek, G.: Confluence as a cut elimination property. In: Nieuwenhuis, R. (ed.) RTA 2003. LNCS, vol. 2706, pp. 2–13. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  20. Futatsugi, K., Nakagawa, A.: An overview of CAFE specification environment – an algebraic approach for creating, verifying, and maintaining formal specifications over networks. In: Proceedings of the 1st IEEE Int. Conference on Formal Engineering Methods (1997)

    Google Scholar 

  21. Goguen, J.A.: How to prove algebraic inductive hypotheses without induction, with applications to the correctness of data type implementation. In: Bibel, W. (ed.) CADE 1980. LNCS, vol. 87, pp. 356–373. Springer, Heidelberg (1980)

    Google Scholar 

  22. Goguen, J.A., Malcolm, G. (eds.): Software Engineering with OBJ: algebraic specification in practice. Advances in Formal Methods, vol. 2. Kluwer Academic Publishers, Boston (2000)

    Google Scholar 

  23. Goguen, J.A., Meseguer, J.: Eqlog: Equality, types, and generic modules for logic programming. In: DeGroot, D., Lindstrom, G. (eds.) Logic Programming: Functions, Relations, and Equations, pp. 295–363. Prentice-Hall, Englewood Cliffs (1986)

    Google Scholar 

  24. Hsiang, J., Rusinowitch, M.: Proving refutational completeness of theorem proving strategies: The transfinite semantic tree method. Journal of the ACM 38(3), 559–587 (1991)

    Article  MATH  MathSciNet  Google Scholar 

  25. Huet, G.: Confluent reductions: Abstract properties and applications to term rewriting systems. Journal of the ACM 27(4), 797–821 (1980)

    Article  MATH  MathSciNet  Google Scholar 

  26. Huet, G.: A complete proof of correctness of the Knuth–Bendix completion algorithm. Journal of Computer and System Sciences 23(1), 11–21 (1981)

    Article  MATH  MathSciNet  Google Scholar 

  27. Huet, G., Lévy, J.-J.: Computations in orthogonal rewriting systems, I. In: Lassez, J.-L., Plotkin, G. (eds.) Computational Logic. ch. 11, pp. 395–414. The MIT press, Cambridge (1991)

    Google Scholar 

  28. Jouannaud, J.-P., Kirchner, H.: Completion of a set of rules modulo a set of equations. SIAM Journal of Computing 15(4), 1155–1194 (1986)

    Article  MATH  MathSciNet  Google Scholar 

  29. Kirchner, C., Kirchner, H.: Rewriting, solving, proving (1999), A preliminary version of a book available at www.loria.fr/~ckirchne/rsp.ps.gz

  30. Kirchner, C., Kirchner, H., Vittek, M.: Designing constraint logic programming languages using computational systems. In: Van Hentenryck, P., Saraswat, V. (eds.) Principles and Practice of Constraint Programming. The Newport Papers. ch. 8, pp. 131–158. The MIT press, Cambridge (1995)

    Google Scholar 

  31. Knuth, D.E., Bendix, P.B.: Simple word problems in universal algebras. In: Leech, J. (ed.) Computational Problems in Abstract Algebra, pp. 263–297. Pergamon Press, Oxford (1970)

    Google Scholar 

  32. Lankford, D.: Canonical inference. Technical report, Louisiana Tech. University (1975)

    Google Scholar 

  33. Le Chenadec, P.: Canonical Forms in Finitely Presented Algebras. John Wiley Sons, Chichester (1986)

    MATH  Google Scholar 

  34. Meseguer, J.: Conditional rewriting logic as a unified model of concurrency. Theoretical Computer Science 96(1), 73–155 (1992)

    Article  MATH  MathSciNet  Google Scholar 

  35. Musser, D.: On proving inductive properties of abstract data types. In: Proceedings, Symposium on Principles of Programming Languages. Association for Computing Machinery, vol. 7 (1980)

    Google Scholar 

  36. Peterson, G., Stickel, M.: Complete sets of reductions for some equational theories. Journal of the ACM 28, 233–264 (1981)

    Article  MATH  MathSciNet  Google Scholar 

  37. Robinson, J.A.: A machine-oriented logic based on the resolution principle. Journal of the ACM 12, 23–41 (1965)

    Article  MATH  Google Scholar 

  38. Rubio, A., Nieuwenhuis, R.: A total AC-compatible ordering based on RPO. Theoretical Computer Science 142(2), 209–227 (1995)

    Article  MATH  MathSciNet  Google Scholar 

  39. Schorlemmer, W.M.: Rewriting logic as a logic of special relations. Electr. Notes Theor. Comput. Sci. 15 (1998)

    Google Scholar 

  40. Stokkermans, K.: A categorical formulation for critical-pair/completion procedures. In: Rusinowitch, M., Remy, J.-L. (eds.) CTRS 1992. LNCS, vol. 656, pp. 328–342. Springer, Heidelberg (1993)

    Google Scholar 

  41. Struth, G.: Canonical Transformations in Algebra, Universal Algebra and Logic. Dissertation, Institut für Informatik, Universität des Saarlandes, Saarbrücken, Germany (June 1998)

    Google Scholar 

  42. Winkler, F.: Knuth-Bendix procedure and Buchberger algorithm - A synthesis. In: Proceedings of the ACM-SIGSAM 1989 International Symposium on Symbolic and Algebraic Computation, Portland, Oregon, USA, pp. 55–67. ACM Press, New York (1989)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Ecole Normale Supérieure de Lyon & LORIA,  

    Guillaume Burel

  2. INRIA & LORIA,  

    Claude Kirchner

Authors
  1. Guillaume Burel
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Claude Kirchner
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Japan Advanced Institute of Science and Technology (JAIST),  

    Kokichi Futatsugi

  2. LIX, Projet INRIA TypiCal, École Polytechnique and CNRS, 91400, Palaiseau, France

    Jean-Pierre Jouannaud

  3. CS Dept., University of Illinois at Urbana-Champaign, USA

    José Meseguer

Rights and permissions

Reprints and permissions

Copyright information

© 2006 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

Burel, G., Kirchner, C. (2006). Completion Is an Instance of Abstract Canonical System Inference. In: Futatsugi, K., Jouannaud, JP., Meseguer, J. (eds) Algebra, Meaning, and Computation. Lecture Notes in Computer Science, vol 4060. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11780274_26

Download citation

  • DOI: https://doi.org/10.1007/11780274_26

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-35462-8

  • Online ISBN: 978-3-540-35464-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation