 As we have already mentioned, soundness is the essential requirement of a calculus while completeness guarantees that all the semantical consequences can be established within the calculus and so the set of validities is recursively enumerable. The most relevant properties for automated deduction are decidability and complexity. 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.