Abstract
Domain independence is an important property of a formula that guarantees that the truth value of the formula in an interpretation remains the same regardless of the underlying domain of the interpretation. Unfortunately, checking domain independence of a first-order formula is in general undecidable. There have been several attempts to define syntactic fragments of first-order logic characterising domain independent formulas that easily can be checked, but all of them are incomplete. We reduce the problem of checking domain independence of a general first-order logic formula to checking a standard first-order logic entail-ment. This method can be applied in any decidable fragment where the formulas participating in the entailment can be expressed.