It is well known that to compute equivalence of two Datalog programs (or equivalently of two first order formulas with the least fixed point operator) wrt all possible inputs and universes, is undecidable. If we fix the universe size to be N, it is clearly decidable in time exponential wrt N. My question is whether one can do better, maybe even in time logarithmic in N (and maybe much worse wrt the length of the programs). Note that equivalence of two nonrecursive Datalog rules can be done in constant time for all inputs, let alone for fixed N, but is NP-Complete wrt the rules' size.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.