---
title: "A Prover for General Inequalities"
authors:
  - "W. W. Bledsoe"
  - "Peter Bruell"
  - "Robert E. Shostak"
doi: ""
url: "https://ijcai.org/proceedings/1979/18"
pdf: "https://ijcai.org/proceedings/1979/0018.pdf"
venue: "Proceedings of the Sixth International Joint Conference on Artificial Intelligence"
year: 1979
pages: ""
track: ""
keywords:
---

# A Prover for General Inequalities

W. W. Bledsoe, Peter Bruell, Robert E. Shostak

*Proceedings of the Sixth International Joint Conference on Artificial Intelligence*.

## Abstract

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.