Proving and rewriting | SpringerLink
Skip to main content
Springer Nature Link
Log in

Proving and rewriting

  • Invited Talk
  • Conference paper
  • First Online:
Algebraic and Logic Programming (ALP 1990)

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

Included in the following conference series:

  • 168 Accesses

Abstract

This paper presents some ways to prove theorems in first and second order logic, such that rewriting does the routine work automatically, and partially successful proofs often return information that suggests what to try next. The theoretical framework makes extensive use of general algebra, and main results include an extension of many-sorted equational logic to universal quantification over functions, some techniques for handling first order logic, and some structural induction principles. The OBJ language is used for illustration, and initiality is a recurrent theme.

The research reported in this paper has been supported in part by grants from the Science and Engineering Research Council, the National Science Foundation, and the System Development Foundation, as well as contracts with the Office of Naval Research and the Fujitsu Corporation.

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

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

References

  1. Robert Boyer and J Moore. A Computational Logic. Academic Press, 1980.

    Google Scholar 

  2. Rod Burstall. Proving properties of programs by structural induction. Computer Journal, 12(1):41–48, 1969.

    Google Scholar 

  3. Rod Burstall and Joseph Goguen. Algebras, theories and freeness: An introduction for computer scientists. In Manfred Wirsing and Gunther Schmidt, editors, Theoretical Foundations of Programming Methodology, pages 329–350. Reidel, 1982. Proceedings, 1981 Marktoberdorf NATO Summer School, NATO Advanced Study Institute Series, Volume C91.

    Google Scholar 

  4. Kokichi Futatsugi, Joseph Goguen, Jean-Pierre Jouannaud, and José Meseguer. Principles of OBJ2. In Brian Reid, editor, Proceedings, Twelfth ACM Symposium on Principles of Programming Languages, pages 52–66. Association for Computing Machinery, 1985.

    Google Scholar 

  5. Kokichi Futatsugi, Joseph Goguen, José Meseguer, and Koji Okada. Parameterized programming in OBJ2. In Robert Balzer, editor, Proceedings, Ninth International Conference on Software Engineering, pages 51–60. IEEE Computer Society Press, March 1987.

    Google Scholar 

  6. Stephen Garland and John Guttag. Inductive methods for reasoning about abstract data types. In Proceedings, Fifteenth Symposium on Principles of Programming Languages, pages 219–229. ACM, January 1988.

    Google Scholar 

  7. Joseph Goguen. How to prove algebraic inductive hypotheses without induction: with applications to the correctness of data type representations. In Wolfgang Bibel and Robert Kowalski, editors, Proceedings, Fifth Conference on Automated Deduction, pages 356–373. Springer-Verlag, 1980. Lecture Notes in Computer Science, Volume 87.

    Google Scholar 

  8. Joseph Goguen. OBJ as a theorem prover, with application to hardware verification. In V.P. Subramanyan and Graham Birtwhistle, editors, Current Trends in Hardware Verification and Automated Theorem Proving, pages 218–267. Springer-Verlag, 1989. Also Technical Report SRI-CSL-88-4R2, SRI International, Computer Science Lab, August 1988.

    Google Scholar 

  9. Joseph Goguen. Principles of parameterized programming. In Ted Biggerstaff and Alan Perlis, editors, Software Reusability, Volume I: Concepts and Models, pages 159–225. Addison-Wesley, 1989.

    Google Scholar 

  10. Joseph Goguen. What is unification? A categorical view of substitution, equation and solution. In Maurice Nivat and Hassan Aït-Kaci, editors, Resolution of Equations in Algebraic Structures, Volume 1: Algebraic Techniques, pages 217–261. Academic Press, 1989. Also Technical Report SRI-CSL-88-2R2, SRI International, Computer Science Lab, August 1988.

    Google Scholar 

  11. Joseph Goguen. Theorem Proving and Algebra. MIT Press, to appear.

    Google Scholar 

  12. Joseph Goguen and Rod Burstall. A study in the foundations of programming methodology: Specifications, institutions, charters and parchments. In Proceedings, Conference on Category Theory and Computer Programming, pages 313–333. Springer-Verlag, 1986. Lecture Notes in Computer Science, Volume 240; also, Report Number CSLI-86-54, Center for the Study of Language and Information, Stanford University, June 1986.

    Google Scholar 

  13. Joseph Goguen and Rod Burstall. Institutions: Abstract model theory for specification and programming. Journal of the Association for Computing Machinery, to appear. Report ECS-LFCS-90-106, Computer Science Department, University of Edinburgh, January 1990; preliminary version, Report CSLI-85-30, Center for the Study of Language and Information, Stanford University, 1985, and remote ancestor, “Introducing Institutions,” in Proceedings, Logics of Programming Workshop, Edward Clarke and Dexter Kozen, editors, Springer-Verlag Lecture Notes in Computer Science, Volume 164, pages 221–256, 1984.

    Google Scholar 

  14. Joseph Goguen, Jean-Pierre Jouannaud, and José Meseguer. Operational semantics of ordersorted algebra. In W. Brauer, editor, Proceedings, 1985 International Conference on Automata, Languages and Programming. Springer-verlag, 1985. Lecture Notes in Computer Science, Volume 194.

    Google Scholar 

  15. Joseph Goguen, Claude Kirchner, Hélène Kirchner, Aristide Mégrelis, and José Meseguer. An introduction to OBJ3. In Jean-Pierre Jouannaud and Stephane Kaplan, editors, Proceedings, Conference on Conditional Term Rewriting, pages 258–263. Springer-Verlag, 1988. Lecture Notes in Computer Science, Volume 308.

    Google Scholar 

  16. Joseph Goguen and José Meseguer. Order-sorted algebra I: Equational deduction for multiple inheritance, overloading, exceptions and partial operations. Technical Report SRI-CSL-89-10, SRI International, Computer Science Lab, July 1989. Given as lecture at Seminar on Types, Carnegie-Mellon University, June 1983; many draft versions exist.

    Google Scholar 

  17. Joseph Goguen and Timothy Winkler. Introducing OBJ3. Technical Report SRI-CSL-88-9, SRI International, Computer Science Lab, August 1988. Revised version to appear with additional authors José Meseguer, Kokichi Futatsugi and Jean-Pierre Jouannaud in Applications of Algebraic Specification using OBJ, edited by Joseph Goguen, Derek Coleman and Robin Gallimore, Cambridge University Press, 1990.

    Google Scholar 

  18. Michael Gordon. Why higher-order logic is a good formalism for specifying and verifying hardware. In George Milne and P.A. Subrahmanyam, editors, Formal Aspects of VLSI Design. North-Holland, 1986.

    Google Scholar 

  19. Robert Harper, Furio Honsell, and Gordon Plotkin. A framework for defining logics. In Proceedings, Second Symposium on Logic in Computer Science, pages 194–204. IEEE Computer Society Press, 1987.

    Google Scholar 

  20. Jieh Hsiang. Refutational Theorem Proving using Term Rewriting Systems. PhD thesis, University of Illinois at Champaign-Urbana, 1981.

    Google Scholar 

  21. Gérard Huet and Derek Oppen. Equations and rewrite rules: A survey. In Ron Book, editor, Formal Language Theory: Perspectives and Open Problems, pages 349–405. Academic Press, 1980.

    Google Scholar 

  22. Jean-Pierre Jouannaud and Hélène Kirchner. Completion of a set of rules modulo a set of equations. Proceedings, 11th Symposium on Principles of Programming Languages, 1984. In SIAM Journal of Computing.

    Google Scholar 

  23. Claude Kirchner, Hélène Kirchner, and José Meseguer. Operational semantics of OBJ3. In Proceedings, 9th International Conference on Automata, Languages and Programming. Springer-Verlag, 1988. Lecture Notes in Computer Science, Volume 241.

    Google Scholar 

  24. Jan Willem Klop. Term rewriting systems: A tutorial. Bulletin of the European Association for Theoretical Computer Science, 32:143–182, June 1987.

    Google Scholar 

  25. David MacQueen and Donald Sannella. Completeness of proof systems for equational specifications. IEEE Transactions on Software Engineering, SE-11(5):454–461, May 1985.

    Google Scholar 

  26. José Meseguer and Joseph Goguen. Initiality, induction and computability. In Maurice Nivat and John Reynolds, editors, Algebraic Methods in Semantics, pages 459–541. Cambridge University Press, 1985.

    Google Scholar 

  27. David Musser. On proving inductive properties of abstract data types. In Proceedings, 7th Symposium on Principles of Programming Languages. Association for Computing Machinery, 1980.

    Google Scholar 

  28. Lawrence C. Paulson. The foundation of a generic theorem prover. Technical Report 130, University of Cambridge, Computer Laboratory, March 1988.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Programming Research Group, Oxford University, SRI International, 94025, Menlo Park, CA

    Joseph A. Goguen

Authors
  1. Joseph A. Goguen
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Hélène Kirchner Wolfgang Wechler

Rights and permissions

Reprints and permissions

Copyright information

© 1990 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Goguen, J.A. (1990). Proving and rewriting. In: Kirchner, H., Wechler, W. (eds) Algebraic and Logic Programming. ALP 1990. Lecture Notes in Computer Science, vol 463. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-53162-9_27

Download citation

  • DOI: https://doi.org/10.1007/3-540-53162-9_27

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-53162-3

  • Online ISBN: 978-3-540-46738-0

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics