If you prove that the theorem prover’s true and false determinations are correct—in the cases in which it can make them—then Bob’s your uncle.