Proving ground confluence and inductive validity in constructor based equational specifications

Abstract

We study ground confluence and inductive validity in equational specifications that are interpreted in a constructor based way. By defining semantics of the specification in an appropriate way, we are able to transfer the proof-by-consistency concepts from unstructured specifications to constructor based specifications, where the unstructured specifications with their usual semantics are included as a special case. We further show that the proof-by-consistency concepts not only apply to inductive theorem proving, but can as well be employed to prove ground confluence of rewrite systems. So we present a refutationally complete prover for ground confluence and inductive validity that applies to unstructured as well as constructor based equational specifications.