|START Conference Manager|
Since non-overlapping equations are valid independently, they are better suitable for the equational proof style usually employed in paper proofs.
We relate the problem to the well-known minimization problem for propositional DNF formulas and show that it is $\Sigma_2^P$-complete. We then develop a concrete algorithm to compute minimal patterns, which naturally generalizes the standard Quine-McCluskey procedure to the domain of term patterns.
START Conference Manager (V2.54.6)