TY - GEN

T1 - Reasoning in systems of equations and inequations

AU - Mohan, Chilukuri K.

AU - Srivas, Mandayam K.

AU - Kapur, Deepak

PY - 1987/1/1

Y1 - 1987/1/1

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=84910762487&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84910762487&partnerID=8YFLogxK

U2 - 10.1007/3-540-18625-5_57

DO - 10.1007/3-540-18625-5_57

M3 - Conference contribution

AN - SCOPUS:84910762487

SN - 9783540186250

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 305

EP - 325

BT - Foundations of Software Technology and Theoretical Computer Science - 7th Conference, Proceedings

A2 - Nori, Kesav V.

PB - Springer Verlag

T2 - 7th Conference on Foundations of Software Technology and Theoretical Computer Science, FST and TCS 1987

Y2 - 17 December 1987 through 19 December 1987

ER -