Completeness of many-sorted equational logic

J. A. Goguen, Jose Meseguer

Research output: Contribution to journalArticle

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.

Original languageEnglish (US)
Pages (from-to)9-17
Number of pages9
JournalACM SIGPLAN Notices
Volume17
Issue number1
DOIs
StatePublished - Jan 1 1982

Fingerprint

Acoustic waves
Abstract data types
Computer science

ASJC Scopus subject areas

  • Software
  • Computer Graphics and Computer-Aided Design

Cite this

Completeness of many-sorted equational logic. / Goguen, J. A.; Meseguer, Jose.

In: ACM SIGPLAN Notices, Vol. 17, No. 1, 01.01.1982, p. 9-17.

Research output: Contribution to journalArticle

Goguen, J. A. ; Meseguer, Jose. / Completeness of many-sorted equational logic. In: ACM SIGPLAN Notices. 1982 ; Vol. 17, No. 1. pp. 9-17.
@article{b398525db85243599fb92ef50a4a473c,
title = "Completeness of many-sorted equational logic",
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.",
author = "Goguen, {J. A.} and Jose Meseguer",
year = "1982",
month = "1",
day = "1",
doi = "10.1145/947886.947887",
language = "English (US)",
volume = "17",
pages = "9--17",
journal = "ACM SIGPLAN Notices",
issn = "1523-2867",
publisher = "Association for Computing Machinery (ACM)",
number = "1",

}

TY - JOUR

T1 - Completeness of many-sorted equational logic

AU - Goguen, J. A.

AU - Meseguer, Jose

PY - 1982/1/1

Y1 - 1982/1/1

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=84976850269&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84976850269&partnerID=8YFLogxK

U2 - 10.1145/947886.947887

DO - 10.1145/947886.947887

M3 - Article

VL - 17

SP - 9

EP - 17

JO - ACM SIGPLAN Notices

JF - ACM SIGPLAN Notices

SN - 1523-2867

IS - 1

ER -