{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,18]],"date-time":"2025-05-18T14:45:58Z","timestamp":1747579558305},"reference-count":43,"publisher":"Cambridge University Press (CUP)","issue":"1","license":[{"start":{"date-parts":[[2009,3,4]],"date-time":"2009-03-04T00:00:00Z","timestamp":1236124800000},"content-version":"unspecified","delay-in-days":5117,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[1995,3]]},"abstract":"<jats:p>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.<\/jats:p>","DOI":"10.1017\/s0960129500000621","type":"journal-article","created":{"date-parts":[[2009,3,4]],"date-time":"2009-03-04T09:00:42Z","timestamp":1236157242000},"page":"9-40","source":"Crossref","is-referenced-by-count":7,"title":["Completeness of category-based equational deduction"],"prefix":"10.1017","volume":"5","author":[{"given":"R\u0103zvan","family":"Diaconescu","sequence":"first","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2009,3,4]]},"reference":[{"key":"S0960129500000621_ref025","unstructured":"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\u2013149.)"},{"key":"S0960129500000621_ref010","unstructured":"Dershowitz N. (1983) Computing with rewrite rules. Technical Report ATR-83(8478)-l, The Aerospace Corp."},{"key":"S0960129500000621_ref024","doi-asserted-by":"publisher","DOI":"10.1098\/rsta.1992.0026"},{"key":"#cr-split#-S0960129500000621_ref023.2","unstructured":"and Technical Report SRI-CSL-89-10, SRI International, Computer Science Lab, July 1989"},{"key":"#cr-split#-S0960129500000621_ref023.4","unstructured":"(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.)"},{"key":"S0960129500000621_ref020","first-page":"307","article-title":"Completeness of many-sorted equational logic","volume":"11","author":"Goguen","year":"1985","journal-title":"Houston Journal of Mathematics"},{"key":"S0960129500000621_ref019","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129500000517"},{"key":"S0960129500000621_ref021","first-page":"295","volume-title":"Logic Programming: Functions, Relations and Equations","author":"Goguen","year":"1986"},{"key":"S0960129500000621_ref018","doi-asserted-by":"crossref","unstructured":"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).","DOI":"10.1007\/3-540-57867-6_1"},{"key":"S0960129500000621_ref015","doi-asserted-by":"crossref","first-page":"357","DOI":"10.1093\/oso\/9780198537601.003.0014","volume-title":"Topology and Category Theory in Computer Science","author":"Goguen","year":"1991"},{"key":"S0960129500000621_ref009","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-57163-9_12"},{"key":"S0960129500000621_ref012","unstructured":"Diaconescu R. (1994) Category-Based Semantics for Equational and Constraint Logic Programming, PhD thesis, Oxford University."},{"key":"S0960129500000621_ref014","unstructured":"Goguen J. (1978) Order sorted algebra. Technical Report 14, UCLA Computer Science Department. Semantics and Theory of Computation Series."},{"key":"S0960129500000621_ref008","unstructured":"Burstall R. and Diaconescu R. (1992) Hiding and behaviour: an institutional approach. Technical Report ECS-LFCS-8892\u2013253, 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)."},{"key":"S0960129500000621_ref016","unstructured":"Goguen J. (1994) Theorem Proving and Algebra, MIT."},{"key":"S0960129500000621_ref005","doi-asserted-by":"publisher","DOI":"10.1007\/BF01692060"},{"key":"S0960129500000621_ref026","doi-asserted-by":"publisher","DOI":"10.1145\/321992.321997"},{"key":"S0960129500000621_ref022","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0014969"},{"key":"S0960129500000621_ref027","unstructured":"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.)"},{"key":"S0960129500000621_ref029","doi-asserted-by":"publisher","DOI":"10.4153\/CMB-1972-055-0"},{"key":"S0960129500000621_ref037","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0030336"},{"key":"S0960129500000621_ref004","volume-title":"Model-Theoretic Logics","author":"Barwise","year":"1985"},{"key":"S0960129500000621_ref007","doi-asserted-by":"publisher","DOI":"10.1017\/S0305004100013463"},{"key":"S0960129500000621_ref006","first-page":"1","article-title":"Structures alg\u00e9briques dans les cat\u00e9gories","volume":"10","author":"Benabou","year":"1968","journal-title":"Cahiers de Topologie et G\u00e9ometrie Diff\u00e9rentiel"},{"key":"S0960129500000621_ref002","volume":"278","author":"Barr","year":"1984","journal-title":"Grundlehren der mathematischen Wissenschafter"},{"key":"S0960129500000621_ref042","volume-title":"A Treatise on Universal Algebra, with Applications, I","author":"Whitehead","year":"1898"},{"key":"S0960129500000621_ref017","doi-asserted-by":"publisher","DOI":"10.1145\/147508.147524"},{"key":"S0960129500000621_ref003","doi-asserted-by":"publisher","DOI":"10.1016\/0003-4843(74)90016-3"},{"key":"S0960129500000621_ref013","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-07142-3_75"},{"key":"S0960129500000621_ref001","first-page":"13","article-title":"A general axiomatizability theorem formulated in terms of cone-injective subcategories","volume":"29","author":"Andr\u00e9ka","year":"1981","journal-title":"Colloquia Mathematics Societas J\u00e1nos Bolyai"},{"key":"S0960129500000621_ref030","doi-asserted-by":"publisher","DOI":"10.1002\/mana.19630270108"},{"key":"S0960129500000621_ref032","doi-asserted-by":"crossref","unstructured":"Lawvere F. W. (1963) Functorial semantics of algebraic theories. Proceedings, National Academy of Sciences, U.S.A., 50:869\u2013872. (Summary of Ph.D. Thesis, Columbia University.)","DOI":"10.1073\/pnas.50.5.869"},{"key":"S0960129500000621_ref031","volume-title":"Abstract and Concrete Categories","author":"Herrlich","year":"1990"},{"key":"S0960129500000621_ref033","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-9839-7"},{"key":"S0960129500000621_ref028","doi-asserted-by":"publisher","DOI":"10.1007\/BF01431492"},{"key":"S0960129500000621_ref034","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-9860-1"},{"key":"S0960129500000621_ref035","doi-asserted-by":"crossref","unstructured":"Mosses P. (1989) Unified algebras and institutions. In: Proceedings, Fourth Annual Conference on Logic in Computer Science, IEEE 304\u2013312.","DOI":"10.1109\/LICS.1989.39185"},{"key":"S0960129500000621_ref040","doi-asserted-by":"publisher","DOI":"10.1016\/0004-3702(85)90029-3"},{"key":"S0960129500000621_ref036","doi-asserted-by":"publisher","DOI":"10.1007\/BF01190411"},{"key":"S0960129500000621_ref038","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(85)90094-5"},{"key":"S0960129500000621_ref041","first-page":"18","article-title":"Many-sorted inferences in automated theorem proving","volume":"418","author":"Walther","year":"1990","journal-title":"Springer-Verlag Lecture Notes in Artificial Intelligence"},{"key":"S0960129500000621_ref039","doi-asserted-by":"publisher","DOI":"10.2307\/2102968"},{"key":"S0960129500000621_ref011","unstructured":"Diaconescu R. (1993) The logic of Horn clauses is equational. Technical Report PRG-TR-3\u201393, Programming Research Group, University of Oxford. (Written in 1990.)"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129500000621","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,3,11]],"date-time":"2024-03-11T01:44:24Z","timestamp":1710121464000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129500000621\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995,3]]},"references-count":43,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1995,3]]}},"alternative-id":["S0960129500000621"],"URL":"https:\/\/doi.org\/10.1017\/s0960129500000621","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[1995,3]]}}}