Forgetting is one of the most important concepts in logic based problem solving, both from a theoretical and a practical point of view. However, the size of the forgetting result is exponential in worst case. To address this issue, we consider the problem of polynomially bounded forgetting, i.e., when the size of the forgetting result can be expressed polynomially. We coin the notion of polynomially bounded forgetting and distinguish several different levels. We then show that forgetting a set of variables under a polynomial bound can be reduced to forgetting a single one. However, checking variable polynomially bounded forgetting is ∑_2~P complete. Hence, we identify some sufficient conditions for this problem. Finally, we consider polynomially bounded forgetting in CNF formulas.
展开▼
