Common equivalence and size after forgetting
This work addresses computational complexity issues in propositional logic for AI and knowledge representation, but it is incremental as it builds on existing concepts like forgetting and equivalence.
The paper tackles the problem of forgetting variables from propositional formulas, which can increase formula size, and explores using common equivalence and variable introduction to shorten formulas. It presents polynomial-space algorithms for forgetting and checking common equivalence in Horn formulas, with polynomial-time results for specific subclasses, and shows NP-hardness for minimization when variables can be introduced.
Forgetting variables from a propositional formula may increase its size. Introducing new variables is a way to shorten it. Both operations can be expressed in terms of common equivalence, a weakened version of equivalence. In turn, common equivalence can be expressed in terms of forgetting. An algorithm for forgetting and checking common equivalence in polynomial space is given for the Horn case; it is polynomial-time for the subclass of single-head formulae. Minimizing after forgetting is polynomial-time if the formula is also acyclic and variables cannot be introduced, NP-hard when they can.