AIMA: Chapter 7, page 216, Global Edition.
An inference algorithm that derives only entailed sentences is called sound or truth preserving. Soundness is a highly desirable property. An unsound inference procedure essentially makes things up as it goes along it announces the discovery of nonexistent needles. It is easy to see that model checking, when it is applicable, is a sound procedure.
I am unable to understand the haystack analogy here. Could someone please provide a better example to explain when inference algorithms are said to be sound?