Hierarchical Reasoning about Inequalities

Book One

Volume

Proceedings of the AAAI Conference on Artificial Intelligence, 6

Engineering Problem Solving

This paper describes a program called BOUNDER that proves inequalities between functions over finite sets of constraints. Previous inequality algorithms perform well on some subset of the elementary functions, but poorly elsewhere. To overcome this problem, BOUNDER maintains a hierarchy of increasingly complex algorithms. When one fails to resolve an inequality, it tries the next. This strategy resolves more inequalities than any single algorithm. It also performs well on hard problems without wasting time on easy ones. The current hierarchy consists of four algorithms: bounds propagation, substitution, derivative inspection, and iterative approximation. Propagation is an extension of interval arithmetic that takes linear time, but ignores constraints between variables and multiple occurrences of variables. The remaining algorithms consider these factors, but require exponential time. Substitution is a new, provably correct, algorithm for utilizing constraints between variables. The final two algorithms analyze constraints between variables. Inspection examines the signs of partial derivatives. Iteration is based on several earlier algorithms from interval arithmetic.