A Prover for General Inequalities
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.
W. W. Bledsoe, Peter Bruell, and Robert E. Shostak. 1979. A Prover for General Inequalities. In Proceedings of the Sixth International Joint Conference on Artificial Intelligence, IJCAI-79. IJCAI, https://ijcai.org/proceedings/1979/18
Bledsoe, W. W., Bruell, P., & Shostak, R. E. (1979). A Prover for General Inequalities. In Proceedings of the Sixth International Joint Conference on Artificial Intelligence, IJCAI-79. IJCAI. https://ijcai.org/proceedings/1979/18
@inproceedings{ijcai1979p18,
title = {A Prover for General Inequalities},
author = {Bledsoe, W. W. and Bruell, Peter and Shostak, Robert E.},
booktitle = {Proceedings of the Sixth International Joint Conference on
Artificial Intelligence, {IJCAI-79}},
publisher = {International Joint Conferences on Artificial Intelligence},
editor = {Bruce G. Buchanan},
year = {1979},
month = {8},
url = {https://ijcai.org/proceedings/1979/18},
}
TY - CPAPER TI - A Prover for General Inequalities AU - Bledsoe, W. W. AU - Bruell, Peter AU - Shostak, Robert E. T2 - Proceedings of the Sixth International Joint Conference on Artificial Intelligence, IJCAI-79 PB - International Joint Conferences on Artificial Intelligence PY - 1979 UR - https://ijcai.org/proceedings/1979/18 ER -Copied
Machine-readable versions of this paper, for tools and AI agents:
