Reconstructing a single-head formula to facilitate logical forgetting
This work provides a complete algorithm for transforming formulas into a single-head format, which is crucial for researchers and practitioners dealing with logical forgetting in propositional definite Horn formulas, enabling more efficient computation.
This paper addresses the computational complexity of logical forgetting, which can be exponential. It introduces a complete algorithm that transforms a given propositional definite Horn formula into an equivalent single-head formula, if one exists, thereby enabling logical forgetting in polynomial time.
Logical forgetting may take exponential time in general, but it does not when its input is a single-head propositional definite Horn formula. Single-head means that no variable is the head of multiple clauses. An algorithm to make a formula single-head if possible is shown. It improves over a previous one by being complete: it always finds a single-head formula equivalent to the given one if any.