Abductive forgetting

Abductive forgetting is removing variables from a logical formula while maintaining its abductive explanations. It is carried in two alternative ways depending on its intended application. Both differ from the usual forgetting, which maintains consequences rather than explanations. Differently from that, abductive forgetting from a propositional formula may not be expressed by any propositional formula. A necessary and sufficient condition tells when it is. Checking it is Pip3-complete. A way to guarantee expressibility of abductive forgetting is to switch from propositional to default logic. Another is to introduce new variables.