# How far meta-logical frameworks are from universal logic?

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.

• What do you mean by "universal logic"? – Martin Berger Sep 27 '16 at 8:52
• 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. – Martin Berger Sep 27 '16 at 8:53
• 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 – TomR Sep 27 '16 at 18:37
• And esspecially habilitation thesis "Institution theory and applications" imar.ro/~diacon/PDF/AbilitareTeza.pdf – TomR Sep 27 '16 at 19:32