 Soundness and completeness are two (metatheoretical) properties of a calculus that are particularly important for automated deduction. Soundness states that the rules of the calculus are truth-preserving. For a direct calculus this means that if Γ ⊢ α then Γ ⊨ α. For indirect calculi, soundness means that if Γ∪{~α} ⊢ ⊥ then Γ ⊨ α. Completeness in a direct calculus states that if Γ ⊨ α then Γ ⊢ α. For indirect calculi, the completeness property is expressed in terms of refutations since one establishes that Γ ⊨ α by showing the existence of a proof, not of α from Γ, but of ⊥ from Γ∪{~α}. Thus, an indirect calculus is refutation complete if Γ ⊨ α implies Γ∪{~α} ⊢ ⊥. Of the two properties, soundness is the most desirable. An incomplete calculus indicates that there are entailment relations that cannot be established within the calculus. For an automated reasoning program this means, informally, that there are true statements that the program cannot prove. Incompleteness may be an unfortunate affair but lack of soundness is a truly problematic situation since an unsound reasoning program would be able to generate false conclusions from perfectly true information.