[Back]

U. Egly, R. Pichler, S. Woltran:
"On Deciding Subsumption Problems";
Talk: Fifth Internternational Symposium on the Theory and Applications of Satisfiability Testing (SAT-02), Cincinnati, Ohio, USA; 2002-05-06 - 2002-05-09; in: "Proceedings of the Fifth International Symposium on the Theory and Applications of Satisfiability Testing (SAT-02)", J. Franco et al. (ed.); (2002), 89 - 97.

Subsumption is an important redundancy elimination method in automated theorem proving. For a given Herbrand universe $H$, it can be strengthened to the clausal H-subsumption, i.e., a clause $D$ over a finite or infinite universe $H$ is H-subsumed by a clause set ${\cal C}$, iff, for every H-ground instance $D \theta$ of $D$, there is a clause $C \in {\cal C}$, such that $C$ subsumes $D\theta$. If the clauses in ${\cal C}$ and the clause $D$ are atoms, then we speak about {\em atomic H-subsumption}.

Clausal and atomic H-subsumption have gained increasing importance in the field of automated model building as recent publications in this field demonstrate. Moreover, problems equivalent to atomic H-subsumption have been studied with different terminologies in many areas of Computer Science.

Both clausal and atomic H-subsumption are known to be intractable, i.e., $\Pi_{2}^{p}$-complete and NP-complete, respectively. In this paper, we present a new approach to deciding (clausal and atomic) H-subsumption that is based on a reduction to QSAT and SAT, respectively.