Reduction contd. Every FOL KB can be propositionalized so as to preserve entailment ● (A ground sentence is entailed by new KB iff entailed by original KB) ● Idea:propositionalize KB and query,apply resolution, return result ● Problem:with function symbols,there are infinitely many nd termsReduction contd. • Every FOL KB can be propositionalized so as to preserve entailment • • (A ground sentence is entailed by new KB iff entailed by original KB) • • Idea: propositionalize KB and query, apply resolution, return result • • Problem: with function symbols, there are infinitely many ground terms