proof or algorithm behind isAlways

I used Matlab isAlways function to show Eigenvalues of a hessian matrix are always positive. I tried to search for any algorithm it may use to convey the proof but I found nothing.

My first question: -How can I use Matlab isAlways function in my research? Is there any proof behind the function? any algorithm behind it?

The Eigenvalues are relatively large and I don't know other ways to proof that they are always positive. I have some assumptions related to Eigenvalues' parameters which cause to Matlab isAlways to output "always positive" in my case.

My second question: -What are alternatives that may help me to proof being always positive based on assumptions? if using Matlab isAlways is not suitable. Example:

assume(x>0)

assumeAlso(beta>0)

isAlways(exp(x)+beta>0)

[George Herson]

To follow on to the above question, How can I learn more about how the isAlways function works? What is its algorithm? What are the names of the related math/logic topics? Thanks.

[Walter Roberson]

x>0 implies x is real. exp() of a real is always non-negative, being 0 only when the value is -inf which is ruled out by x>0 . beta>0 implies beta is real and non-negative. Non-negative plus non-negative is always > 0.

Answer 1

[George Herson]

isAlways() can immediately return items like 7>5 as true, but those that need it are (heuristically) simplified on both sides. Then the rhs is subtracted from the lhs and the difference compared with zero. If they're equal, true is returned from an equation, and false from a ≠ relation. Other relations are treated similarly (lhs - rhs) and related to zero, per the relop they specify. E.g., a greater-than relation is asked if (lhs - rhs) > 0, the answer simplified, and if its a Boolean, that is returned. If no Boolean results from this gauntlet, the result is how ever an undecidable result is handled.