Variable Elimination and Chaining in a Resolution-based Prover for Inequalities.

W. W. Bledsoe, Larry M. Hines

Browse the full CADE paper archive.