A Decidability Result about Sufficient-Completeness of Axiomatically
Specified Abstract Data Types
Tobias Nipkow, Gerhard Weikum
The problem of deciding whether an axiomatic specification of an abstract
data type is sufficiently-complete is known to be in general unsolvable.
Regarding axioms as directed rewrite rules instead of symmetric equations, a
specification defines a reduction relation on terms. It is proved that in the
subclass of left-linear axiomatic specifications the property of
sufficient-completeness is decidable if the corresponding reduction relation
is normalizing and confluent.
SpringerLink
BibTeX:
<![CDATA[
@inproceedings{Nipkow-Weikum,
author={Tobias Nipkow and Gerhard Weikum},
title={A Decidability Result about Sufficient-Completeness of Axiomatically
Specified Abstract Data Types},
editors={A.B. Cremers and H.P. Kriegel},
booktitle={Proc.\ 6th GI-Conf.\ Theoretical Computer Science},
year=1983,publisher=Springer,series=LNCS,volume=145,pages={257--268}}
]]></plaintext></p></div></div>