Inference rules and proof procedures for inequations

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

Research output: Contribution to journalArticle

1 Scopus citations

Abstract

The negation of equality is an important relation that arises naturally in the study of equational programming languages and logic programming with equality. Proving and solving equations and inequations may also constitute subtasks in constraint logic programming. In this paper, we give forward (i.e., nonrefutational) techniques for proving the negation of equality in a theory. We develop a complete inference system to check whether an inequation is a logical consequence of a given system of equations and inequations. The inference system is used to develop a goal-directed semidecision procedure which uses a narrowing technique for proving inequations. A decision procedure is obtained when certain additional conditions are satisfied. The semidecision procedure for proving inequations is also modified to obtain a semidecision procedure for solving inequations in a theory, i.e., finding a substitution such that the corresponding instance of the given inequation is a logical consequence of the given system.

Original languageEnglish (US)
Pages (from-to)75-104
Number of pages30
JournalThe Journal of Logic Programming
Volume9
Issue number1
DOIs
StatePublished - Jul 1990

ASJC Scopus subject areas

  • Logic

Fingerprint Dive into the research topics of 'Inference rules and proof procedures for inequations'. Together they form a unique fingerprint.

  • Cite this