Abstract
This paper introduces ORM2 plus – a new linear syntax and complete semantics expressed in first order logic of ORM2 – which can be shown correctly embedding the original proposal. A provably correct encoding of the core fragment ORM2 zero in the ALCQIALCQI description logic (a fragment of OWL2 with qualified cardinality restrictions and inverse roles) is presented. Complexity of reasoning on ORM2 conceptual schemas, and the ExpTime-membership of reasoning on ORM2 zero , are also shown. On the basis of these results, a systematic critique of alternative approaches to the formalisation of ORM2 in (description) logics published so far is provided. A prototype has been implemented providing a backend for the automated support of implicit constraints deduction, schema consistency checks, and user-defined constraints entailment, for ORM2 zero conceptual schemas along with its translation into ALCQIALCQI knowledge bases.