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.

  • 1
    $\begingroup$ This link cs.cmu.edu/Groups/AI/areas/reasonng/defeasbl/dprolog/0.html is for D-Prolog, which might be useful. The page says "an extension of Prolog implementing defeasible reasoning". This page sciencedirect.com/science/article/pii/016792369090005C is an abstract for a paper that talks about a DSS implemented in d-prolog. $\endgroup$ – Χpẘ Apr 23 '17 at 0:52
  • 1
    $\begingroup$ You can certainly represent the metatheoretical reasoning in even a relatively weak system like LF (e.g. as implemented by Elf or Twelf) let alone a rather powerful system like the Calculus of Inductive Constructions. This is probably what "implementing" actually means for you unless you want a system like Prolog or some constructive interpretation. It's quite possible you could even (non-trivially) embed these logics into Twelf/Coq so that you can leverage the metatheoretic machinery those implementations already have. For example, there are embeddings of linear logic into LF. $\endgroup$ – Derek Elkins Apr 23 '17 at 3:28

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.