Completeness and Soundness Theorem(Completeness and Soundness) o a is a tableau provable from S+ a is a logical consequence of s o If we take a to be any contradiction such as B AnB in 1, we see that s is inconsistent if and only if s is unsatisfiableCompleteness and Soundness . Theorem (Completeness and Soundness) . . 1. α is a tableau provable from S ⇔ α is a logical consequence of S. 2. If we take α to be any contradiction such as β ∧ ¬β in 1, we see that S is inconsistent if and only if S is unsatisfiable. Yi Li (Fudan University) Discrete Mathematics June 4, 2013 10 / 17