Reasoning in systems of equations and inequations

Chilukuri K. Mohan, Mandayam K. Srivas, Deepak Kapur

Research output: Chapter in Book/Report/Conference proceedingConference contribution

1 Scopus citations

Abstract

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.

Original languageEnglish (US)
Title of host publicationFoundations of Software Technology and Theoretical Computer Science - 7th Conference, Proceedings
EditorsKesav V. Nori
PublisherSpringer Verlag
Pages305-325
Number of pages21
ISBN (Print)9783540186250
DOIs
StatePublished - Jan 1 1987
Externally publishedYes
Event7th Conference on Foundations of Software Technology and Theoretical Computer Science, FST and TCS 1987 - Pune, India
Duration: Dec 17 1987Dec 19 1987

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume287 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other7th Conference on Foundations of Software Technology and Theoretical Computer Science, FST and TCS 1987
CountryIndia
CityPune
Period12/17/8712/19/87

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Reasoning in systems of equations and inequations'. Together they form a unique fingerprint.

  • Cite this

    Mohan, C. K., Srivas, M. K., & Kapur, D. (1987). Reasoning in systems of equations and inequations. In K. V. Nori (Ed.), Foundations of Software Technology and Theoretical Computer Science - 7th Conference, Proceedings (pp. 305-325). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 287 LNCS). Springer Verlag. https://doi.org/10.1007/3-540-18625-5_57