Contents    Page-10    Prev    Next    Page+10    Index   

Soundness and Completeness

The notation p ⊨ q is read ``p entails q''; it means that q holds in every model in which p holds.

The notation p ⊢m q means that q can be derived from p by some proof mechanism m.

A proof mechanism m is sound if p ⊢m q → p ⊨ q.

A proof mechanism m is complete if p ⊨ q → p ⊢m q.

Resolution for predicate calculus is:

We generally are not willing to give up soundness, since we want our conclusions to be valid. We might be willing to give up completeness: if a sound proof procedure will prove the theorem we want, that is enough.