Not too Big, Not too Small ... Complexities of Fixed-Domain Reasoning in First-Order and Description Logics

From International Center for Computational Logic

Toggle side column

Not too Big, Not too Small ... Complexities of Fixed-Domain Reasoning in First-Order and Description Logics

Sebastian RudolphSebastian Rudolph,  Lukas SchweizerLukas Schweizer
Sebastian Rudolph, Lukas Schweizer
Not too Big, Not too Small ... Complexities of Fixed-Domain Reasoning in First-Order and Description Logics
In Alessandro Artale, Birte Glimm and Roman Kontchakov, eds., Proceedings of the 30th International Workshop on Description Logics, volume 1879 of CEUR Workshop Proceedings, July 2017. CEUR-WS.org
  • KurzfassungAbstract
    We consider reasoning problems in description logics and variants of first-order logic under the fixed-domain semantics, where the model size is finite and explicitly given. It follows from previous results that standard reasoning is NP-complete for a very wide range of logics, if the domain size is given in unary encoding. In this paper, we complete the complexity overview for unary encoding and investigate the effects of binary encoding with partially surprising results. Most notably, fixed-domain standard reasoning becomes NExpTime for the rather low-level description logics ELI and ELF (as opposed to ExpTime when no domain size is given). On the other hand, fixed-domain reasoning remains NExpTime even for first-order logic, which is undecidable under the unconstrained semantics. For less expressive logics, we establish a generic criterion ensuring NP-completeness of fixed-domain reasoning. Amongst other logics, this criterion captures all the tractable profiles of OWL 2.
  • Projekt:Project: QuantLA
  • Forschungsgruppe:Research Group: Computational LogicComputational Logic
@inproceedings{RS2017,
  author    = {Sebastian Rudolph and Lukas Schweizer},
  title     = {Not too Big, Not too Small ... Complexities of Fixed-Domain
               Reasoning in First-Order and Description Logics},
  editor    = {Alessandro Artale and Birte Glimm and Roman Kontchakov},
  booktitle = {Proceedings of the 30th International Workshop on Description
               Logics},
  series    = {CEUR Workshop Proceedings},
  volume    = {1879},
  publisher = {CEUR-WS.org},
  year      = {2017},
  month     = {July}
}