TY - JOUR

T1 - Inference rules and proof procedures for inequations

AU - Mohan, Chilukuri K.

AU - Srivas, Mandayam K.

AU - Kapur, Deepak

PY - 1990/7

Y1 - 1990/7

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

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

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

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

U2 - 10.1016/0743-1066(90)90034-3

DO - 10.1016/0743-1066(90)90034-3

M3 - Article

AN - SCOPUS:0025462561

VL - 9

SP - 75

EP - 104

JO - The Journal of Logic Programming

JF - The Journal of Logic Programming

SN - 0743-1066

IS - 1

ER -