UNIFICATION MODULO ACI + 1 + 0
Paliath Narendran · Fundamenta Informaticae · 1996
We show that elementary ACI10 unification is in P, even with constant restrictions. As a corollary, we prove that validity of quantified Horn formulae can be tested in O(n 2 ) time. Solvability of elementary disunification problems modulo ACI10 is shown to be NP-hard.