Thanks, I think this is a good example of what I'm looking for. One key ingredient is the presence of a logic inference engine (and not for type inference only

Thanks, I think this is a good example of what I'm looking for. One key ingredient is the presence of a logic inference engine (and not for type inference only, as in Coq, Haskell). - If your system doesn't have a logic inference engine, it's a vanilla proof-assistant (Coq). - If it has one, it's one of two: - a partially-automated theorem prover, (Isabelle) - a fully-automated theorem prover P.S.: Wait a minute. It just occurred to me, is Coq using its Hindley-Milner Type Inference engine as a Logic Inference engine for verifying constructed proofs of theorems and propositions? (is that the killer idea?)