Are there logics that can not be implemented in current logical frameworks like Coq. Why those logics can not be implemented? And what should be improved in existing logical frameworks/proof assistants to allow implementation of those logics as well.
The question is about properties and types of such non-implementable logics. But specifically I am researching non-monotonic, defeasible, adaptable logics and I don't know whether should I give effort to implement them in Coq (or other prood assistant) and should I seek other logical frameworks (maybe there are small but powerful ones) or should respect those logics as two strange and implement from the scratch in some programming language.
By "implementation" I mean creating theorem prover, satisfiability checker.