Solving problems by formula manipulation in logic and linear inequalities

摘要

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.