A prover for general inequalities
Woodrow W. Bledsoe, Peter Bruell, Robert E. Shostak · International Joint Conference on Artificial Intelligence · 1979
A variation of an earlier prover (described in Machine Intelligence 8) is used to prove theorems about general inequalities, i.e., first-order logic with equality where the only predicate symbols are <, <, and =, and where function symbols are admitted. Transcripts of some proofs are given.