DLML: logic descriptions

Description logics are very modular (one constructor can be added to a logic together with the corresponding inference rules). The difficult point in designing DTDs for DL is to preserve that modularity and being able to assemble the operators described individualy in a logic description.

We start by describing a solution for describing the logic in a natural way and generating automatically and syntactic (DTD) and semantic (DSD) description of the logic (in progress). Then we propose as set of already available XML descriptions (plus DTD and DSD) for well-known logics. Last, the particularity of designing modular DTDs for description logics are presented.

The DLML DTD

The above description constrains the logic designer to directly produce a DTD with the precise guidelines. For improving this situation, we are currently designing a way of providing the logic description in XML. This have several advantage:

• A more user friendly way to desribe the logic;
• The opportunity to generate not only the syntactic description (DTD) of the logic but also its semantic description (DSD) and maybe more (e.g. theorem prover).

For that purpose, use:

Logics available so far

It must be noted that there can be several ways to define the same logic (in the semantic sense). For instance, it is well known that ALC and ALUE are equivalent. As far as possible, we try to give only one below (with the maximum number of constructors available) and to elicit the other constructions.
Below are provided the XML descripton of the logic (through the DLML DTD) and the generated (so far, hand-made) DTD and DSD.

fl-.xml - dtd - manual dtd - dsd

For the FL- system (with and, all, some).

fl.xml - dtd - manual dtd - dsd

For the FL system (with and, all, some, range).

al.xml - dtd - manual dtd - dsd

For the AL system (with and, all, some, anything, nothing, anot).

fln.xml - dtd - manual dtd - dsd

For the FLN system (with and, all, some, range, atleast, atmost).

aln.xml - dtd - manual dtd - dsd

For the ALN system (with and, all, some, anything, nothing, anot, atleast, atmost)

alu.xml - dtd - manual dtd - dsd

For the ALU system (with and, all, some, anything, nothing, anot, or).

ale.xml - dtd - manual dtd - dsd

For the ALE system (with and, all, some, anything, nothing, anot, csome).

alr.xml - dtd - manual dtd - dsd

For the ALR system (with and, all, some, anything, nothing, anot, androle).

alun.xml - dtd - manual dtd - dsd

For the ALUN system (with and, all, some, anything, nothing, anot, or, atleast, atmost).

alc.xml - dtd - manual dtd - dsd

For the ALC system (with and, all, some, anything, nothing, anot, not, or).

alen.xml - dtd - manual dtd - dsd

For the ALEN system (with and, all, some, anything, nothing, anot, csome, atleast, atmost).

alur.xml - dtd - manual dtd - dsd

For the ALUR system (with and, all, some, anything, nothing, anot, or, androle).

aler.xml - dtd - manual dtd - dsd

For the ALER system (with and, all, some, anything, nothing, anot, csome, androle).

alnr.xml - dtd - manual dtd - dsd

For the ALNR system (with and, all, some, anything, nothing, anot, atleast, atmost, androle).

alcn.xml - dtd - manual dtd - dsd

For the ALCN system (with and, all, some, anything, nothing, anot, not, or, atleast, atmost).

alunr.xml - dtd - manual dtd - dsd

For the ALUNR system (with and, all, some, anything, nothing, anot, or, atleast, atmost, androle).

alcr.xml - dtd - manual dtd - dsd

For the ALCR system (with and, all, some, anything, nothing, anot, not, or, androle).

alenr.xml - dtd - manual dtd - dsd

For the ALENR system (with and, all, some, anything, nothing, anot, csome, atleast, atmost, androle).

alncr.xml - dtd - manual dtd - dsd

For the ALNCR system (with and, all, some, anything, nothing, anot, not, or, atleast, atmost, androle).

aluni.xml - dtd - manual dtd - dsd

For the ALUNI system (with and, all, some, anything, nothing, anot, or, atleast, atmost, inv).

s.xml - dtd - dsd

For the S system (with and, all, csome, anything, nothing, not, or, trans).

shi.xml - dtd - dsd

For the SHI system (with and, all, csome, anything, nothing, not, or, inv, trans).

shq.xml - dtd - dsd

For the SHQ system (with and, all, csome, anything, nothing, not, or, catleast, catmost, trans).

shiq.xml - dtd - dsd

For the SHIQ system (with and, all, csome, anything, nothing, not, or, catleast, catmost, inv, trans).

bigr.xml - dtd - manual dtd - dsd

For the R system (with androle, comp, self, notrole).

bigu.xml - dtd - manual dtd - dsd

For the U system (with and, all, or, not, some, csome, atleast, atmost, single, catleast, catmost, anything, nothing, rvm, sameas, anot, androle, orrole, notrole, comp, trans, inv, self, domain, range).

DTD design

This section is not compulsory for understanding the way DLML works. It remains here for historical reasons and because it gives a hint of the modtivations for the particular encoding we use.

First, each operator is defined in a single DTD, then a logic is defined by importing all the required DTDs. For this to work, "global" constants and definers have to be "declared" and bound just when assembling the logic DTD.

This leads to the following decomposition of the declaration of a particular description logic:

• Import of the constant elements (CATOM and RATOM both defined by the atom DTD).
• Definition of the CDESC and RDESC entities by declaring all the allowed constructors (plus the above CATOM and RATOM). These entities are refered to by the following imports.
• Import the constructors (see list here).
• Definition of the FORM entity by declaring all the allowed formula introducers. FORM is used in the TERMINOLOGY element.
• Import the formula introducers (see list here).