Completeness of many-sorted equational logic
- 1 January 1982
- journal article
- Published by Association for Computing Machinery (ACM) in ACM SIGPLAN Notices
- Vol. 17 (1), 9-17
- https://doi.org/10.1145/947886.947887
Abstract
The rules of deduction which are usually used for many-sorted equational logic in computer science, for example in the study of abstract data types, are not sound. Correcting these rules by introducing explicit quantifiers yields a system which, although it is sound, is not complete; some new rules are needed for the addition and deletion of quantifiers. This note is intended as an informal, but precise, introduction to the main issues and results. It gives an example showing the unsoundness of the usual rules; it also gives a completeness theorem for our new rules, and gives necessary and sufficient conditions for the old rules to agree with the new.Keywords
This publication has 4 references indexed in Scilit:
- Equations and Rewrite Rules: A SurveyPublished by Elsevier ,1980
- Heterogeneous algebrasJournal of Combinatorial Theory, 1970
- Algebras with a Scheme of OperatorsMathematische Nachrichten, 1963
- On the Structure of Abstract AlgebrasMathematical Proceedings of the Cambridge Philosophical Society, 1935