### 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 language | English (US) |
---|---|

Pages (from-to) | 75-104 |

Number of pages | 30 |

Journal | The Journal of Logic Programming |

Volume | 9 |

Issue number | 1 |

DOIs | |

State | Published - 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

*The Journal of Logic Programming*,

*9*(1), 75-104. https://doi.org/10.1016/0743-1066(90)90034-3