Skip to main content
SpringerLink
Log in

About proofs by consistency

Abstract

  • Conference paper
  • First Online:
Rewriting Techniques and Applications (RTA 1998)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1379))

Included in the following conference series:

  • 207 Accesses

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

Access this chapter

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 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.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

Institutional subscriptions

References

  1. L. Bachmair. Proof by consistency in equational theories. In Proc. 3rd IEEE Symp. Logic in Computer Science, Edinburgh, July 1988.

    Google Scholar 

  2. L. Bachmair. Canonical Equational Proofs. Birkhäuser, Boston, 1991.

    Book  MATH  Google Scholar 

  3. A.-C. Caron, J.-L. Coquidé, and M. Dauchet. Encompassment properties and automata with constraints. In C. Kirchner, editor, 5th International Conference on Rewriting Techniques and Applications, volume 690 of Lecture Notes in Computer Science, Montreal, Canada, June 1993. Springer-Verlag.

    Google Scholar 

  4. H. Comon and F. Jacquemard. Ground reducibility is exptime-complete. In Proc. IEEE Symp. on Logic in Computer Science, Varsaw, June 1997. IEEE Comp. Soc. Press.

    Google Scholar 

  5. L. Pribourg. A narrowing procedure for theories with constructors. In R. Shostak, editor, Proc. 7th Int. Conf. on Automated Deduction, volume 170 of Lecture Notes in Computer Science, pages 259–281, Napa, CA., 1984. Springer-Verlag.

    Google Scholar 

  6. L. Fribourg. A strong restriction of the inductive completion procedure. Journal of Symbolic Computation, 8:253–276, 1989.

    Article  MathSciNet  MATH  Google Scholar 

  7. J. A. Goguen. How to prove inductive hypothesis without induction. In Proc. 5th Conf. on Automated Deduction, Les Arcs, France, LNCS 87, July 1980.

    Google Scholar 

  8. G. Huet and J.-M. Hullot. Proofs by induction in equational theories with constructors. J. Comput. Syst. Sci., 25(2), 1982.

    Google Scholar 

  9. J.-P. Jouannaud and A. Bouhoula. Automata-driven automated induction. In Twelfth Annual IEEE Symposium on Logic in Computer Science, Warsaw, Poland, June 1997. IEEE Comp. Soc. Press.

    Google Scholar 

  10. J.-P. Jouannaud and E. Kounalis. Automatic proofs by induction in equational theories without constructors. In Proc. 1st IEEE Symp. Logic in Computer Science, Cambridge, Mass., June 1986.

    Google Scholar 

  11. J.-P. Jouannaud and E. Kounalis. Automatic proofs by induction in theories without constructors. Information and Computation, 82(1), July 1989.

    Google Scholar 

  12. D. Kapur and D. Musser. Proof by consistency. Artificial Intelligence, 31(2), Feb. 1987.

    Google Scholar 

  13. D. Kapur, P. Narendran, D. Rosenkrantz, and H. Zhang. Sufficient completeness, ground reducibility and their complexity. Acta Inf., 28:311–350, 1991.

    Article  MathSciNet  MATH  Google Scholar 

  14. D. Kapur, P. Narendran, and H. Zhang. On sufficient completeness and related properties of term rewriting systems. Acta Inf., 24(4):395–415, 1987.

    Article  MathSciNet  MATH  Google Scholar 

  15. D. Kapur and H. Zhang. An overview of the rewrite rule laboratory. Journal of Mathematics of Computation, 1995.

    Google Scholar 

  16. W. Küchlin. Inductive completion by ground proof transformation. In H. Ait-Kaci and M. Nivat, editors, Proc. Coll. on the Resolution of Equations in Algebraic Structures, Lakeway. Academic Press, May 1987.

    Google Scholar 

  17. E. Kounalis. Testing for the ground (co)-reducibility in term rewriting systems. Theoretical Computer Science, 106(1):87–117, 1992.

    Article  MathSciNet  MATH  Google Scholar 

  18. D. S. Lankford. A simple explanation of inductionless induction. Technical Report MTP-14, Mathematics Department, Louisiana Tech. Univ., 1981.

    Google Scholar 

  19. D. Musser. Proving inductive properties of abstract data types. In Proc. 7th ACM Symp. on Principles of Programming Languages, Las Vegas, 1980.

    Google Scholar 

  20. U. Reddy. Term rewriting induction. In Proc. 10th Int. Conf. on Automated Deduction, Kaiserslautern, LNCS 449, 1990.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Laboratoire Spécification et Vérification, URA 2236 du CNRS école Normale Supérieure de Cachan, 61 avenue du président Wilson, 94235, Cachan cedex, France

    Hubert Comon

Authors
  1. Hubert Comon
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Tobias Nipkow

Rights and permissions

Reprints and permissions

Copyright information

© 1998 Springer-Verlag

About this paper

Cite this paper

Comon, H. (1998). About proofs by consistency. In: Nipkow, T. (eds) Rewriting Techniques and Applications. RTA 1998. Lecture Notes in Computer Science, vol 1379. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0052366

Download citation

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

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-64301-2

  • Online ISBN: 978-3-540-69721-3

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation