ein Verfahren, mit dem festgestellt werden kann, ob aus den (prädikatenlogischen) Aussagen A₁, ..., A_n die Aussage K folgt. Hierzu werden A₁, ..., A_n und K in die Klauselform überführt, d. h. als Disjunktionen von negierten oder unnegierten Atomaussagen (Aussagen, die keine logischen Partikel enthalten) dargestellt. Zu je zwei