Thumbnail
Access Restriction
Subscribed

Author Nelson, Greg ♦ Oppen, Derek C.
Source ACM Digital Library
Content type Text
Publisher Association for Computing Machinery (ACM)
File Format PDF
Copyright Year ©1980
Language English
Subject Domain (in DDC) Computer science, information & general works ♦ Data processing & computer science
Abstract The notion of the congruence closure of a relation on a graph is defined and several algorithms for computing it are surveyed. A simple proof is given that the congruence closure algorithm provides a decision procedure for the quantifier-free theory of equality. A decision procedure is then given for the quantifier-free theory of LISP list structure based on the congruence closure algorithm. Both decision procedures determine the satisfiability of a conjunction of literals of length $\textit{n}$ in average time $\textit{O}(\textit{n}$ log $\textit{n})$ using the fastest known congruence closure algorithm. It is also shown that if the axiomatization of the theory of list structure is changed slightly, the problem of determining the satisfiability of a conjunction of literals becomes NP-complete. The decision procedures have been implemented in the authors' simplifier for the Stanford Pascal Verifier.
ISSN 00045411
Age Range 18 to 22 years ♦ above 22 year
Educational Use Research
Education Level UG and PG
Learning Resource Type Article
Publisher Date 1980-04-01
Publisher Place New York
e-ISSN 1557735X
Journal Journal of the ACM (JACM)
Volume Number 27
Issue Number 2
Page Count 9
Starting Page 356
Ending Page 364


Open content in new tab

   Open content in new tab
Source: ACM Digital Library