ML Anthology

A Prover for General Inequalities

W. W. Bledsoe, Peter Bruell, Robert E. Shostak
IJCAI 1979 pp. 66-69
/ijcai/1979/bledsoe1979ijcai-prover/

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.

Semantic Scholar

Cite

Text

Bledsoe et al. "A Prover for General Inequalities." International Joint Conference on Artificial Intelligence, 1979.

Markdown

[Bledsoe et al. "A Prover for General Inequalities." International Joint Conference on Artificial Intelligence, 1979.](https://mlanthology.org/ijcai/1979/bledsoe1979ijcai-prover/)

BibTeX

@inproceedings{bledsoe1979ijcai-prover,
  title     = {{A Prover for General Inequalities}},
  author    = {Bledsoe, W. W. and Bruell, Peter and Shostak, Robert E.},
  booktitle = {International Joint Conference on Artificial Intelligence},
  year      = {1979},
  pages     = {66-69},
  url       = {https://mlanthology.org/ijcai/1979/bledsoe1979ijcai-prover/}
}