Simultaneous Checking of Completeness and Ground 
Confluence




Algebraic specifications provide a powerful method 
for the specification of abstract data types 
in programming languages and software systems. Completeness 
and ground confluence are fundamental notions for 
building algebraic specifications in a correct and 
modular way. Related work for checking ground 
confluence is based on completion techniques or 
on the test that all critical pairs 
between axioms are valid w.r.t. a sufficient 
criterion for ground confluence. It is generally 
accepted that such techniques may be very 
inefficient even for very small specifications. Indeed, 
the completion procedure often diverges and there 
often exist many critical pairs of the 
axioms. In this paper, we present a 
procedure for simultaneously checking completeness and ground 
confluence for specifications with free/non-free constructors and 
parameterized specifications. If the specification is not 
complete or not ground confluent, then our 
procedure will output the set of patterns 
on whose ground instances a function is 
not defined and it can easily identify 
the rules that break ground confluence. Our 
procedure is the first one which is 
complete and always terminates under the assumption 
of an oracle for deciding (joinable-) inductive 
properties. In contrast to previous work, our 
method does not rely on completion techniques 
and does not require the computation of 
critical pairs of the axioms. The method 
has been implemented in the prover SPIKE. 
This system allowed us to prove the 
completeness and the groun confluence of many 
specifications in a completely automatic way where 
related techniques diverge or generate very complex 
proofs.