I am investigating metalogical-frameworks like Isabelle/Pure (very few information), http://twelf.org/wiki/Main_Page, http://abella-prover.org/ for encoding of new logics. And natural question arises - how far those frameworks are from universal logic? I am especially interested their capabilities to encode defeasible deontic logic and monoidal categorical logics.

  • $\begingroup$ What do you mean by "universal logic"? $\endgroup$ – Martin Berger Sep 27 '16 at 8:52
  • 1
    $\begingroup$ It should be possible to embed any reasonable logic into Isabelle/Pure, since Isabelle/Pure is a meta-logic, designed to embed other logics. Alternatively, you can use any prover to do a deep embedding of your target logic. The main question is pragmatic: how much proof automation can you get for your target logic? Deep embeddings tend to be quite terrible in this regard. $\endgroup$ – Martin Berger Sep 27 '16 at 8:53
  • $\begingroup$ By universal logic I mean endeavours that are described in book series and journal Studies in Universal Logic and Logica Universalis link.springer.com/journal/11787 springer.com/series/7391 Specifically I mean institution theory springer.com/gp/book/9783764387075 $\endgroup$ – TomR Sep 27 '16 at 18:37
  • $\begingroup$ And esspecially habilitation thesis "Institution theory and applications" imar.ro/~diacon/PDF/AbilitareTeza.pdf $\endgroup$ – TomR Sep 27 '16 at 19:32

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.