# Efficiently decidable logics

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:

1. Decision procedure for membership in set of theorems is efficent
2. More expressive than PL (but not nearly as expressive as Tarski's logic)
3. Not just practical but formally efficient
• Perhaps I misunderstand what you wrote, but did you just say that SAT is in P? If so - then no, it isn't (to our knowledge). First, in general the conversion to CNF is exponential, and again exponential to DNF, but even if you start with a CNF formula, the problem is NP-complete. – Shaull Apr 15 '15 at 5:49
• No SAT is not in P (probably), determining if the negation of a sentence is SAT is in P however which is sufficient for determining if a formula is a theorem or not. theorems of PL do not have SAT negations. – Jake Apr 15 '15 at 5:52
• Also note that converting the negation of a CNF to a DNF is very easy. Just flip operator (and/or operators) and negate atoms. Additionally the conversion to CNF need only be equisatisfiable. – Jake Apr 15 '15 at 6:02
• 1) No, converting to DNF is not "easy". Well, it's conceptually simple but since the resulting formulat can be exponentially large, it's not efficient. 2) You claim co-SAT is in P but SAT is not. That is a contradiction since P is closed against complement. 3) It is not per se clear what "deciding a logic" means. Do you solve the word problem for formulae (syntactically)? Do you decide satisfiability, validity, or any other property? Without further qualification, one would assume the first. – Raphael Apr 15 '15 at 9:11
• Your question is riddled with so many misconceptions that I doubt you will understand and/or appreciate any answer. Which is no, afaik; I don't know of an even marginally expressive logic whose set of theorems (valid formulae, tautologies) is decidable. – Raphael Apr 15 '15 at 9:13