Speeding up algorithms on atomic representations of Herbrand models via new redundancy criteria (Q5927983)

The paper studies two important decision problems regarding models: the equivalence of two models and the truth evaluation of a clause under a given interpretation. NEWLINENEWLINENEWLINESpecifically, algorithms are presented for both problems, in the case of Herbrand models given through atomic representations. NEWLINENEWLINENEWLINEAn atomic representation of a Herbrand model over a Herbrand universe \(H\) is a set \(\mathcal{A}=\{A_1, \dots, A_n\}\) of atoms on \(H\) such that a ground atom evaluates to `true' if and only if it is an instance of some atoms in \(\mathcal A\). NEWLINENEWLINENEWLINEGottlob-Pichler proved that both problems are coNP-complete for the special case of linear atomic representations even in the absence of function symbols. This means that no polynomial solution can be expected unless P=NP; in this paper, the source of complexity is analysed to be the number of atoms (rather than the total length of the input problem) and this information is used to provide more efficient algorithms by using redundancy criteria.