A logic is decidable when there is an algorithm that answer YES or NO in a finite time to the question: is the formula \(\varphi\) valid? As validity and satisfiability are interdefinible (\(\models \varphi\) iff \(\lnot \varphi\) is not satisfiable) this problem is often called the satisfiability problem. Among the basic tasks a computer is asked for are satisfiability and model checking. Propositional logic is decidable but first-order logic, many-sorted version included, is undecidable. Howe