I have new logic which has syntax and semantics in usual natural languages and I have to create theorem prover/solver/reasoner for this logic. Is there framework or tool set that can generate such prover from the formal definition of grammar and semantics? I have heard about Isabelle/HOL, is this right set of tools. Is such generation a common path to proceed. Are the metalogical framework, prover compilers suitable for any kind of new logic?
Of course, I can create parser and encode all the algorithms by myself from scratch but this is not the common practice, I guess?