Access Restriction

Author Meseguer, J. ♦ Goguen, J. A.
Source ACM Digital Library
Content type Text
Publisher Association for Computing Machinery (ACM)
File Format PDF
Language English
Subject Domain (in DDC) Computer science, information & general works ♦ Computer programming, programs & data
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.
Description Affiliation: SRI International, Menlo Park CA (Goguen, J. A.; Meseguer, J.)
Age Range 18 to 22 years ♦ above 22 year
Educational Use Research
Education Level UG and PG
Learning Resource Type Article
Publisher Date 1983-05-01
Publisher Place New York
Journal ACM SIGPLAN Notices (SIGP)
Volume Number 17
Issue Number 1
Page Count 9
Starting Page 9
Ending Page 17

Open content in new tab

   Open content in new tab
Source: ACM Digital Library