David Carral


CRCN Researcher at Inria within the Sophia Antipolis - Méditerranée Centre


Member of the GraphIK team, the LIRMM, the University of Montpellier, and the CNRS




Born in 1989; Spanish national; based in Montpellier, France; photo from 2021

Broadly speaking, I am interested in the study of logical languages (mostly first-order logic, existential rules, and Description Logics) and their theoretical/computational properties. More precisely, here are some research questions that I am looking into these days:
  • If a first-order logic (FOL) theory without equality is FO-rewritable or has the bounded-treewidth model property, does it also have the finite model property?
  • If a FOL theory is FO-rewritable and has the universal model finite property, is it also uniformly bounded?
  • What are the expressivity limits of FOL languages that are decidable or semi-decidable?
  • What is the query complexity of solving Boolean query entailment over FOL theories that are FO-rewritable?
  • What is the undecidability status of checking if a FOL theory is FO-rewritable?
  • Can we develop a logic that characterises P? If so, is it less expressive than existential second-order logic?
If you know anything about the above (or just feel like discussing a bit), you should contact me.

Moreover, I am also interested in the implementation of efficient reasoning algorithms. In the past, I participated in the development of VLog, which is an implementation of the chase procedure. In the future, I intend to participate in the development of Graal, which is a Java toolkit dedicated to querying knowledge bases within the framework of existential rules.

Top 5 papers; newest first:
To download any materials that I published before 2021, check out my previous personal page. For everything else, see the links below:

I am always looking for students who are intrinsically motivated to work on some research topic that I also find interesting. I propose some such topics below but if you are interested in working on something else (and you think that I may also be interested in it), feel free to contact me about it.
  • Development of sufficient conditions for termination and non-termination of the chase algorithm.
  • Study of consequence-preserving normalisation procedures that transform FOL theories into theories of disjunctive existential rule sets.
  • Implementation of the core chase for DL ontologies and guarded FOL theories.

I am not doing much teaching at the moment. For more information about my teaching experience, check my CV or have a look under the "Teaching" tab in my previous personal page.

• From 9/07 to 8/11:

European Degree in Computer Engineering at Universidad Pontificia de Salamanca

• From 9/11 to 8/12:

Master of Science in Computer Science at Wright State University

• From 9/12 to 10/16:

Ph.D. in Computer Science and Engineering at Wright State University

• From 5/13 to 12/13:

Recognised Student at University of Oxford

• From 11/16 to 12/20:

Posdoctoral Researcher at Technische Universität Dresden

• From 1/21 onwards:

CRCN Researcher at Inria

Click here to download the full version.

  • At the end of 2021, I organised a seminar about Decidable Fragments of Horn First-Order Logic.
  • I am the organiser of the biweekly group seminar of my research team (that is, GraphIK). For more info about the content of this seminar, check out this link; if you would like to present something, do send me an email (we can arrange an online presentation).

Important News:

We (Pierre Bisquert, Federico Ulliana, and me) are looking for a PhD student to work on this topic within our research project R4Agri. If you have any questions about it, contact us!