Figure 1. Functions for deciding the existence of solutions.

Developer` and Experimental` contexts are put on $ContextPath so that we do not need to prepend them to the function names.

This shows that is nonnegative for all real x and y.

Let us define two classes of inequalities.

This shows that i1[2/3] and i2[2/3] have no common solutions.

Here is a graphical representation of the problem. Solutions of i1 are colored blue and solutions of i2 are colored red.

This shows that i1[1/3] and i2[1/3] have common solutions.

Here is a graphical representation of the problem. Solutions of i1 are colored blue and solutions of i2 are colored red.

The next example is based on a problem formulated by T. Ono in 1914. He conjectured that for all triangles the following inequality is true.

The variables a, b, and c are lengths of sides of the triangle, and F is its area. A counterexample was found by G. Quijano in 1915. We can generate a counterexample using InequalityInstance.

For acute triangles the conjecture is true, and the proof was given by F. Balitrand in 1916. Here is a proof using ImpliesRealQ.

[Article Index] [Prev Page][Next Page]