Proving and rewriting. (English) Zbl 1496.03045
Kirchner, Hélène (ed.) et al., Algebraic and logic programming. Second international conference, Nancy, France, October 1–3, 1990. Proceedings. Berlin etc.: Springer-Verlag. Lect. Notes Comput. Sci. 463, 1-24 (1990).
Summary: 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.
For the entire collection see [Zbl 0763.68011].
For the entire collection see [Zbl 0763.68011].
MSC:
| 03B35 | Mechanization of proofs and logical operations |
| 08A70 | Applications of universal algebra in computer science |
| 68Q42 | Grammars and rewriting systems |
References:
| [1] | Robert Boyer and J Moore. A Computational Logic. Academic Press, 1980. |
| [2] | Rod Burstall. Proving properties of programs by structural induction. Computer Journal, 12(1):41-48, 1969. · Zbl 0164.46202 |
| [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. · Zbl 0518.68009 |
| [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. |
| [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. |
| [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. |
| [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. · Zbl 0438.68043 |
| [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. |
| [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. |
| [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. |
| [11] | Joseph Goguen. Theorem Proving and Algebra. MIT Press, to appear. |
| [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. · Zbl 0615.68002 |
| [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. |
| [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. · Zbl 0591.68041 |
| [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. · Zbl 0666.68010 |
| [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. · Zbl 0778.68056 |
| [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. |
| [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. · Zbl 0612.94015 |
| [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. · Zbl 0778.03004 |
| [20] | Jieh Hsiang. Refutational Theorem Proving using Term Rewriting Systems. PhD thesis, University of Illinois at Champaign-Urbana, 1981. · Zbl 0657.68097 |
| [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. |
| [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. |
| [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. · Zbl 0649.68028 |
| [24] | Jan Willem Klop. Term rewriting systems: A tutorial. Bulletin of the European Association for Theoretical Computer Science, 32:143-182, June 1987. · Zbl 0666.68025 |
| [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. · Zbl 0558.68017 |
| [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. · Zbl 0571.68004 |
| [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. |
| [28] | Lawrence C. Paulson. The foundation of a generic theorem prover. Technical Report 130, University of Cambridge, Computer Laboratory, March 1988. · Zbl 0679.68173 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
