Reduction contd. Theorem:Herbrand(1930).If a sentence a is entailed by an FOL KB,it is entailed by a finite subset of the propositionalized KB ldea:Forn=0to∞do create a propositional KB by instantiating with depth-$n$terms see if a is entailed by this KB Problem:works if a is entailed,loops if a is not entailed Theorem:Turing (1936),Church(1936)Entailment for FOL is semidecidable(algorithms exist that say yes to every entailed sentence,but no algorithm exists that also says no to every nonentailed sentence.) Reduction contd. Theorem: Herbrand (1930). If a sentence α is entailed by an FOL KB, it is entailed by a finite subset of the propositionalized KB Idea: For n = 0 to ∞ do create a propositional KB by instantiating with depth-$n$ terms see if α is entailed by this KB Problem: works if α is entailed, loops if α is not entailed Theorem: Turing (1936), Church (1936) Entailment for FOL is semidecidable (algorithms exist that say yes to every entailed sentence, but no algorithm exists that also says no to every nonentailed sentence.)