Hostname: page-component-599cfd5f84-z6fpd Total loading time: 0 Render date: 2025-01-07T07:11:12.726Z Has data issue: false hasContentIssue false
  • English
  • Français

Completeness of category-based equational deduction

Published online by Cambridge University Press:  04 March 2009

Răzvan Diaconescu
Răzvan Diaconescu
Affiliation:
Programming Research Group, Oxford University, Great Britain
Get access Rights & Permissions [Opens in a new window]

Abstract

Equational deduction is generalised within a category-based abstract model theory framework, and proved complete under a hypothesis of quantifier projectivity, using a semantic treatment that regards quantifiers as models rather than variables, and valuations as model morphisms rather than functions. Applications include many- and order-sorted (conditional) equational logics, Horn clause logic, equational deduction modulo a theory, constraint logics, and more, as well as any possible combination among them. In the cases of equational deduction modulo a theory and of constraint logic the completeness result is new. One important consequence is an abstract version of Herbrand's Theorem, which provides an abstract model theoretic foundation for equational and constraint logic programming.

Type
Research Article
Information
Mathematical Structures in Computer Science , Volume 5 , Issue 1 , March 1995 , pp. 9 - 40
Copyright
Copyright © Cambridge University Press 1995

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

Andréka, H. and Németi, I. (1981) A general axiomatizability theorem formulated in terms of cone-injective subcategories. In: Csakany, B., Fried, E. and Schmidt, E. T. (eds.) Universal Algebra. Colloquia Mathematics Societas János Bolyai 29, North-Holland 13–35.Google Scholar
Barr, M. and Wells, C. (1984) Toposes, Triples and Theories. Grundlehren der mathematischen Wissenschafter 278, Springer-Verlag.Google Scholar
Barwise, J. (1974) Axioms for abstract model theory. Annals of Mathematical Logic 7 221–265.CrossRefGoogle Scholar
Barwise, J. and Feferman, S. (1985) Model-Theoretic Logics, Springer-Verlag.Google Scholar
Bauderon, M. and Courcelle, B. (1987) Graph expressions and graph rewritings. Math. Systems Theory 20.CrossRefGoogle Scholar
Benabou, J. (1968) Structures algébriques dans les catégories. Cahiers de Topologie et Géometrie Différentiel 10 1–126.Google Scholar
Birkhoff, G. (1935) On the structure of abstract algebras. Proceedings of the Cambridge Philosophical Society 31 433–454.CrossRefGoogle Scholar
Burstall, R. and Diaconescu, R. (1992) Hiding and behaviour: an institutional approach. Technical Report ECS-LFCS-8892–253, Laboratory for Foundations of Computer Science, University of Edinburgh. (Also in: A Classical Mind: Essays in Honour of C.A.R. Hoare, Prentice Hall, 1993).Google Scholar
Cazanescu, V. (1993) Local equational logic. In: Esik, Z. (ed.) Proceedings, 9th International Conference on Fundamentals of Computation Theory FCT'93. Springer-Verlag Lecture Notes in Computer Science 710 162–170.CrossRefGoogle Scholar
Dershowitz, N. (1983) Computing with rewrite rules. Technical Report ATR-83(8478)-l, The Aerospace Corp.Google Scholar
Diaconescu, R. (1993) The logic of Horn clauses is equational. Technical Report PRG-TR-3–93, Programming Research Group, University of Oxford. (Written in 1990.)Google Scholar
Diaconescu, R. (1994) Category-Based Semantics for Equational and Constraint Logic Programming, PhD thesis, Oxford University.Google Scholar
Goguen, J. (1974) Semantics of computation. In: Manes, E. G. (ed.) Proceedings, First International Symposium on Category Theory Applied to Computation and Control 234–249. University of Massachusetts at Amherst. (Also in: Springer-Verlag Lecture Notes in Computer Science (1975) 25 151–163.)CrossRefGoogle Scholar
Goguen, J. (1978) Order sorted algebra. Technical Report 14, UCLA Computer Science Department. Semantics and Theory of Computation Series.Google Scholar
Goguen, J. (1991) Types as theories. In: Reed, G. M., Roscoe, A. W and Wachter, R. F. (eds.) Topology and Category Theory in Computer Science 357–390, Oxford. (Proceedings of a Conference held at Oxford, June 1989.)CrossRefGoogle Scholar
Goguen, J. (1994) Theorem Proving and Algebra, MIT.Google Scholar
Goguen, J. and Burstall, R. (1992) Institutions: Abstract model theory for specification and programming. Journal of the Association for Computing Machinery 39 (1) 95–146. (Draft appears as Report ECS-LFCS-90–106, Computer Science Department, University of Edinburgh, January 1990; an early ancestor is ‘Introducing Institutions’ in: Clarke, E. and Kozen, D. (eds.) (1984) Proceedings, Logics of Programming Workshop, Springer- Verlag Lecture Notes in Computer Science 164 221–256.CrossRefGoogle Scholar
Goguen, J. and Diaconescu, R. (1993) Towards an algebraic semantics for the object paradigm. In: Proceedings, Tenth Workshop on Abstract Data Types, Springer-Verlag (to appear).CrossRefGoogle Scholar
Goguen, J. and Diaconescu, R. (1994) An Oxford survey of order sorted algebra. Mathematical Structures in Computer Science 4 363–392.CrossRefGoogle Scholar
Goguen, J. and Meseguer, J. (1985) Completeness of many-sorted equational logic. Houston Journal of Mathematics 11 (3) 307–334. (Preliminary versions have appeared in: SIGPLAN Notices (1981) 16 (7) 24–37; SRI Computer Science Lab, Report CSL-135, May 1982; and Report CSLI-84–15, Center for the Study of Language and Information, Stanford University, September 1984.)Google Scholar
Goguen, J. and Meseguer, J. (1986) Eqlog: Equality, types, and generic modules for logic programming. In: DeGroot, D. and Lindstrom, G. (eds.) Logic Programming: Functions, Relations and Equations, Prentice-Hall 295–363. (An earlier version appears in Journal of Logic Programming, (1984) 1 (2) 179–210.)Google Scholar
Goguen, J. and Meseguer, J. (1987) Models and equality for logical programming. In: Ehrig, H., Levi, G., Kowalski, R. and Montanari, U. (eds.) Proceedings, 1987 TAPSOFT, Springer-Verlag Lecture Notes in Computer Science 250 1–22.CrossRefGoogle Scholar
Goguen, J. and Meseguer, J. (1992) Order-sorted algebra I: Equational deduction for multiple inheritance, overloading, exceptions and partial operations. Theoretical Computer Science 105 (2) 217–273. (Also: Programming Research Group Technical Monograph PRG-80, Oxford University, December 1989; and Technical Report SRI-CSL-89–10, SRI International, Computer Science Lab, July 1989; originally given as lecture at Seminar on Types, Carnegie-Mellon University, June 1983; many draft versions exist, from as early as 1985.)Google Scholar
Goguen, J., Stevens, A., Hobley, K. and Hilberdink, H. (1992) 20BJ, a metalogical framework based on equational logic. Philosophical Transactions of the Royal Society, Series A 339 69–86. (Also in: Hoare, C. A. R. and Gordon, M. J. C. (eds.) (1992) Mechanized Reasoning and Hardware Design, Prentice-Hall 69–86.)Google Scholar
Goguen, J., Thatcher, J. and Wagner, E. (1976) An initial algebra approach to the specification, correctness and implementation of abstract data types. Technical Report RC 6487, IBM T. J. Watson Research Center. (Also in: Yeh, R. (ed.) (1978) Current Trends in Programming Methodology, IV, Prentice-Hall 80–149.)Google Scholar
Goguen, J., Thatcher, J., Wagner, E. and Wright, J. (1977) Initial algebra semantics and continuous algebras. Journal of the Association for Computing Machinery, 24 (1) 68–95. (An early version is ‘Initial Algebra Semantics’, with James Thatcher, IBM T.J. Watson Research Center, Report RC 4865, May 1974.)CrossRefGoogle Scholar
Goguen, J., Winkler, T., Meseguer, J., Futatsugi, K. and Jouannaud, J.-P. (1994) Introducing OBJ. In: Goguen, J. (ed.) Algebraic Specification with OBJ: An Introduction with Case Studies, Cambridge (to appear). (Also to appear as Technical Report from SRI International.)Google Scholar
Hatcher, W. S. (1970) Quasiprimitive categories. Math. Ann. 190 93–96.CrossRefGoogle Scholar
Herrlich, H. and Ringel, C. M. (1972) Identities in categories. Can. Math. Bull. 15 297–299.CrossRefGoogle Scholar
Higgins, P. J. (1963) Algebras with a scheme of operators. Mathematische Nachrichten 27 115–132.CrossRefGoogle Scholar
Herrlich, H., Adamek, J. and Strecker, G. (1990) Abstract and Concrete Categories, John Wiley & Sons.Google Scholar
Lawvere, F. W. (1963) Functorial semantics of algebraic theories. Proceedings, National Academy of Sciences, U.S.A., 50:869–872. (Summary of Ph.D. Thesis, Columbia University.)CrossRefGoogle Scholar
Mac Lane, S. (1971) Categories for the Working Mathematician, Springer-Verlag.CrossRefGoogle Scholar
Manes, E. (1976) Algebraic Theories, Springer-Verlag Graduate Texts in Mathematics 26.CrossRefGoogle Scholar
Mosses, P. (1989) Unified algebras and institutions. In: Proceedings, Fourth Annual Conference on Logic in Computer Science, IEEE 304–312.CrossRefGoogle Scholar
Rodenburg, P. H. (1991) A simple algebraic proof of the equational interpolation theorem. Algebra Universalis 28 48–51.CrossRefGoogle Scholar
Tarlecki, A. (1984) Free constructions in algebraic institutions. In: Chytil, M. P. and Koubek, V.(eds.) Proceedings, International Symposium on Mathematical Foundations of Computer Science. Springer-Verlag Lecture Notes in Computer Science 176 526–534. (Extended version: University of Edinburgh, Computer Science Department, Report CSR-149–83; and revised version ‘On the existence of Free Models in Abstract Algebraic Institutions’, September 1984.)CrossRefGoogle Scholar
Tarlecki, A. (1986) On the existence of free models in abstract algebraic institutions. Theoretical Computer Science 37 269–304. (Preliminary version, University of Edinburgh, Computer Science Department, Report CSR-165–84.)CrossRefGoogle Scholar
Tarski, A. (1944) The semantic conception of truth. Philos. Phenomenological Research 4 13–47.CrossRefGoogle Scholar
Walther, C. (1985) A mechanical solution of Schubert's steamroller problem by many-sorted resolution. Artificial Intelligence 26 (2) 217–214.CrossRefGoogle Scholar
Walther, C. (1990) Many-sorted inferences in automated theorem proving. In: Sorts and Types in Artificial Intelligence. Springer-Verlag Lecture Notes in Artificial Intelligence 418 18–48.Google Scholar
Whitehead, A. N. (1898) A Treatise on Universal Algebra, with Applications, I, Cambridge. (Reprinted 1960.)Google Scholar