title: API for theorem proving strategies
body: <p>Are there high-level API/environments/libraries for testing the effectiveness of a particular approach (e.g. heuristic algorithm) for generating constructive proofs based on first-order logic/type theory?</p>
  <p>I am trying to find a user-friendly API that can verify the correctness of proofs for formulas such as: <img src="https://latex.codecogs.com/gif.latex?%5Cforall%20a%20%5Cin%20%5Cmathbb%7BN%7D.%5C%20%5Cexists%20b%20%5Cin%20%5Cmathbb%7BN%7D.%5C%20b%20%3E%20a" alt="" />.</p>
  <p>If possible, I'd prefer standalone libraries instead of direct interface for languages like Coq/HOL.</p>
  <p>Thanks in advance!</p>