Abstract
We study the properties of semantic consequence in a particular subset of first-order logic with equality and no function symbols, under the unique name assumption. Formulas in this subset of logic are rules of form $\forall \vec x (H \rightarrow \exists \vec y C) where the hypothesis $H$ and the conclusion $C$ are conjunctions of atoms (possibly with equality), $\vec x$ contains the variables in $H$ and $\vec y$ the variables in $C$ that are not in $H$. This subset is particularly expressive since it can encode a universal Turing machine, at the cost of decidability of reasoning. We propose new decidable subclasses of this problem, by combining restrictions on both the structure of the rules themselves and the structure of the interactions between rules, encoded in the graph of rule dependencies. The most general decidable subclass presented here is based on a mixed forward/backward chaining algorithm. Finally, we relate our rules to other notions (tuple-generating dependencies in databases, conceptual graph rules, the TBox in description logics) and explain how the associated deduction problems could benefit from our results.