Some Structural Properties of the Logic of Rules

Jean-François Baget 1, 2 Marie-Laure Mugnier 2 Michel Leclère 2 Eric Salvat 3
2 GRAPHIK - Graphs for Inferences on Knowledge
LIRMM - Laboratoire d'Informatique de Robotique et de Microélectronique de Montpellier, CRISAM - Inria Sophia Antipolis - Méditerranée
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.
Document type :
Complete list of metadatas

Cited literature [13 references]  Display  Hide  Download
Contributor : Jean-François Baget <>
Submitted on : Friday, June 20, 2008 - 10:24:14 AM
Last modification on : Wednesday, June 5, 2019 - 11:58:13 AM
Long-term archiving on : Friday, May 28, 2010 - 6:36:29 PM


Files produced by the author(s)


  • HAL Id : lirmm-00289250, version 1


Jean-François Baget, Marie-Laure Mugnier, Michel Leclère, Eric Salvat. Some Structural Properties of the Logic of Rules. RR-08016, 2008. ⟨lirmm-00289250⟩



Record views


Files downloads