Common equivalence and size after forgetting

Abstract

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.

References in corpus (5)

• Space Efficiency of Propositional Knowledge Representation Formalisms
• When You Must Forget: beyond strong persistence when forgetting in answer set programming
• A Syntactic Operator for Forgetting that Satisfies Strong Persistence
• One head is better than two: a polynomial restriction for propositional definite Horn forgetting
• Graph Width Measures for CNF-Encodings with Auxiliary Variables

Cited by in corpus (1)

• One head is better than two: a polynomial restriction for propositional definite Horn forgetting