Solving Problems by Formula Manipulation in Logic and Linear Inequalities
Abstract
Using formal logic, many problems from the general area of linear inequalities can be expressed in the elementary theory of addition on the real numbers (EAR). We describe a method for eliminating quantifiers in EAR which has been programmed and demonstrate its usefulness in solving some problems related to linear programming. In the area of mechanical mathematics this kind of approach has been neglected in favor of more generalized methods based on Herbrand expansion. However, in a restricted area, such as linear inequalities, the use of these specialized methods can increase efficiency by several orders of magnitude over an axiomatic Herbrand approach, and make practical problems accessible.
Cite
Text
Hodes. "Solving Problems by Formula Manipulation in Logic and Linear Inequalities." International Joint Conference on Artificial Intelligence, 1971. doi:10.1016/0004-3702(72)90046-XMarkdown
[Hodes. "Solving Problems by Formula Manipulation in Logic and Linear Inequalities." International Joint Conference on Artificial Intelligence, 1971.](https://mlanthology.org/ijcai/1971/hodes1971ijcai-solving/) doi:10.1016/0004-3702(72)90046-XBibTeX
@inproceedings{hodes1971ijcai-solving,
title = {{Solving Problems by Formula Manipulation in Logic and Linear Inequalities}},
author = {Hodes, Louis},
booktitle = {International Joint Conference on Artificial Intelligence},
year = {1971},
pages = {553-559},
doi = {10.1016/0004-3702(72)90046-X},
url = {https://mlanthology.org/ijcai/1971/hodes1971ijcai-solving/}
}