Generalizing Redundancy in Propositional Logic: Foundations and Hitting Sets Duality
This foundational work addresses the problem of simplifying propositional formulas for applications in AI and other domains, but it is incremental as it builds on existing redundancy concepts.
The authors developed a generalized theoretical framework for labeled CNF formulas to unify various extensions of redundancy detection and removal in propositional logic, such as handling redundant groups or variables, and derived results that subsume and extend previous work.
Detection and elimination of redundant clauses from propositional formulas in Conjunctive Normal Form (CNF) is a fundamental problem with numerous application domains, including AI, and has been the subject of extensive research. Moreover, a number of recent applications motivated various extensions of this problem. For example, unsatisfiable formulas partitioned into disjoint subsets of clauses (so-called groups) often need to be simplified by removing redundant groups, or may contain redundant variables, rather than clauses. In this report we present a generalized theoretical framework of labelled CNF formulas that unifies various extensions of the redundancy detection and removal problem and allows to derive a number of results that subsume and extend previous work. The follow-up reports contain a number of additional theoretical results and algorithms for various computational problems in the context of the proposed framework.