Z3 is a state-of-the art theorem prover from microsoft research. see the z3 package for a detailed description.

this package can be used to invoke z3 via its java api.