Vorträge und Posterpräsentationen (mit Tagungsband-Eintrag):
U. Egly, R. Pichler, S. Woltran:
"On Deciding Subsumption Problems";
Vortrag: Fifth Internternational Symposium on the Theory and Applications of Satisfiability Testing (SAT-02),
Cincinnati, Ohio, USA;
06.05.2002
- 09.05.2002; in: "Proceedings of the Fifth International Symposium on the Theory and Applications of Satisfiability Testing (SAT-02)",
J. Franco et al. (Hrg.);
(2002),
S. 89
- 97.
Kurzfassung englisch:
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.
Erstellt aus der Publikationsdatenbank der Technischen Universität Wien.