This is not really meant as a critique, more of a general suggestion for implementers to improve their docs. As someone who teaches logic and works with standar

This is not really meant as a critique, more of a general suggestion for implementers to improve their docs. As someone who teaches logic and works with standard logics from time to time (HOL with Lambek Calculus, normal and classical modal logics, and plain old FOL), I've found it unnecessarily hard to figure out from the docs with what logics you can implement in them, whether you can just load these and use them, how to enter formulas, how to prove things, how to construct models, etc. This all seems overcomplicated in these tools, and almost all of them seem to mix up completely unrelated programming languages with logic. Couldn't this all be simpler? I understand that the typical use cases for these solvers are different. Still, I often wish there was a tool that I can just fire up, choose modal logic EMC from a menu and check whether a certain formula is a theorem. So far, it has always turned out easier for me to do this by hand than using a theorem prover.