Reasoning in systems of equations and inequations

Reasoning in purely equational systems has been studied quite extensively in recent years. Equational reasoning has been applied to several interesting problems, such as, development of equational programming languages, automating induction proofs, and theorem proving. However, reasoning in the presence of explicit inequations is still not as well understood. The expressive power of equational languages will be greatly enhanced if one is allowed to state inequations of terms explicitly. In this paper, we study reasoning in systems which consist of equations as well as inequations, emphasizing the development of forward, i.e., non-refutational, techniques for deducing valid inequations, similar to those for equational inference. Such techniques can be used as a basis for developing execution strategies for equational and declarative languages. We develop an inference system and show that it is complete for deducing all valid inequations. The inference system is used to develop a goal-directed semi-decision procedure which uses a narrowing technique for proving inequations. This semi-decision procedure can be converted into a decision procedure when certain additional conditions are satisfied.