So propositional logic (PL) is efficiently (in P) decidable because I can convert formulas to an equisatisifiable CNF-formula, negate and convert (efficiently, by De Morgans laws) to DNF. I can then efficiently see if this formula is satisfiable. If it is satisfiable then my original formula was not a theorem. PL is however not super expressive.
On the other hand some more expressive logics like tarski's theory of real closed fields is decidable but in an absolutely absurd amount of time.
Somewhere in between is certain modal logics like GL and K that have PSPACE-complete decidability.
In the middle I know about practically efficiently decidable logics like those handled by SMT solvers. But these are not formally efficient decision procedures. No matter how good they become I can always find some pathological case.
Are the more expressive logics that are formally efficiently decidable? To put it in bullets are there any logics that have the following properties:
- Decision procedure for membership in set of theorems is efficent
- More expressive than PL (but not nearly as expressive as Tarski's logic)
- Not just practical but formally efficient