TY - JOUR

T1 - Inference rules and proof procedures for inequations

AU - Mohan, Chilukuri K.

AU - Srivas, Mandayam K.

AU - Kapur, Deepak

N1 - Funding Information:
Address cormspondence to Dr. C. K. Mohan, School of Computer and Information Science, University, Syracuse. NY 13244. Received Msy 1987; accepted August 1988. *Research supported in part by the National Science Foundation Grant MCS8401624. ‘Odyssey Research Associates, 301A Harris B. Dates Drive, Ithaca, NY 14850. ‘Research supported in part by the National Science Foundation Grant CCR8408461. address: Computrrr Science Dept., SUNY at Albany, NY 12222.

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

SN - 0743-1066

VL - 9

SP - 75

EP - 104

JO - The Journal of Logic Programming

JF - The Journal of Logic Programming

IS - 1

ER -