DOLA

This is an experiment for the Syntax Matters research topic.

see Lola-2 and Talk:DOLA for how this was created

⚠️ LLM-generated content notice: Parts of this page may have been created or edited with the assistance of a large language model (LLM). The prompts that have been used might be on the page itself, the discussion page or in straight forward cases the prompt was just "Write a mediawiki page on X" with X being the page name. While the content has been reviewed it might still not be accurate or error-free.

DOLA: A Description Ontology Language

Inspired by N. Wirth's Lola-2

DOLA is a notation for specifying ontologies in the tradition of OWL Description Logic. In many ways it resembles Lola-2: where Lola describes static circuits, DOLA describes conceptual domains. Objects in a description are classes (sets of individuals), properties (relations), and individuals (concrete entities). Class expressions combine classes and property restrictions using operators that mirror the logical gates of Lola.

---

0. Vocabulary

Special characters:

~ & | = # < <= > >= ( ) [ ] { } <: := . , ; : o

Reserved words:

BEGIN BOT CLASS CONST DATA DIFF DISJOINT END EXACT FUNC
IND IFUNC IMPORT INVERSE MAX MIN ONLY ONTOLOGY PROP RANGE
DOMAIN REFL IRREFL SAME SELF SOME SYM ASYM TOP TRANS VALUE CHAIN

---

1. Identifiers, IRIs, and Comments

Identifiers denote classes, properties, individuals, and constants.

identifier = letter {letter | digit}.
 iri        = "<" {character} ">".
integer    = digit {digit}.
string     = '"' {character} '"'.
literal    = integer | string.

Capital and lower-case letters are considered distinct. IRIs (Internationalized Resource Identifiers) reference external ontologies.

Comments are enclosed by (* and *) and may occur between any two symbols.

---

2. Classes and Datatypes

Every individual belongs to one or more classes. The universal class is TOP (owl:Thing); the empty class is BOT (owl:Nothing).

classRef = identifier | "TOP" | "BOT".
datatype = "INT" | "FLOAT" | "STRING" | "BOOL" | identifier.

The predeclared datatypes INT, FLOAT, STRING, and BOOL correspond to xsd:integer, xsd:float, xsd:string, and xsd:boolean respectively.

---

3. Constant Declarations

ConstDeclaration = identifier "=" integer ";".

Constants may be used wherever an integer is expected, for example in cardinality restrictions.

---

4. Class Expressions

Class expressions define classes by combining atomic classes with operators representing set-theoretic constructions and property restrictions. Whereas Lola expressions define signal values through gates, DOLA expressions define classes through set-theoretic and relational constructors.

classExpr   = classTerm {"|" classTerm}.
classTerm   = classFactor {"&" classFactor}.
classFactor = classAtom
            | "~" classFactor
            | restriction
            | "{" identifier {"," identifier} "}"
            | "(" classExpr ")".
classAtom   = identifier | "TOP" | "BOT".

restriction = ("SOME" | "ONLY") identifier ["." classFactor]
            | ("MIN" | "MAX" | "EXACT") integer identifier ["." classFactor]
            | "VALUE" identifier identifier
            | "SELF" identifier.

When the "." classFactor of a restriction is omitted, it defaults to TOP.

Operators (in order of increasing precedence):

Operator	Meaning	DL Notation
	class union	<math>C \sqcup D</math>
&	class intersection	<math>C \sqcap D</math>
~	class complement	<math>\lnot C</math>

Restrictions construct classes from properties:

Restriction	Meaning	DL Notation
SOME R . C	existential — has at least one <math>R</math>-filler in <math>C</math>	<math>\exists R.C</math>
ONLY R . C	universal — all <math>R</math>-fillers are in <math>C</math>	<math>\forall R.C</math>
MIN n R . C	minimum qualified cardinality	<math>\geq n\; R.C</math>
MAX n R . C	maximum qualified cardinality	<math>\leq n\; R.C</math>
EXACT n R . C	exact qualified cardinality	<math>= n\; R.C</math>
VALUE R a	has-value — has <math>R</math>-filler <math>a</math>	<math>\exists R.\{a\}</math>
SELF R	has-self — is <math>R</math>-related to itself	<math>\exists R.\mathsf{Self}</math>

The enumeration {a, b, c} denotes the class containing exactly the named individuals <math>a</math>, <math>b</math>, <math>c</math> (OneOf).

Examples:

Person & Male                                         (* intersection *)
Doctor | Lawyer                                       (* union *)
~Parent                                               (* complement *)
SOME hasChild . Person                                (* existential *)
ONLY hasChild . (Doctor | Lawyer)                     (* universal *)
MIN 2 hasChild                                        (* unqualified min card. *)
Person & SOME hasChild . (SOME hasChild . Person)     (* nesting *)
{mon, tue, wed, thu, fri}                             (* enumeration *)

---

5. Class Declarations

ClassDeclaration = identifier ["=" classExpr | "<:" classExpr] ";".

A bare identifier (e.g. Person;) introduces a named class with no axioms. The symbol = specifies an equivalent class (necessary and sufficient conditions). The symbol <: specifies a superclass (necessary conditions only).

The distinction is fundamental: <math>A = C</math> means an individual is an <math>A</math> if and only if it satisfies <math>C</math>; <math>A <: C</math> means every <math>A</math> satisfies <math>C</math>, but satisfying <math>C</math> does not entail being an <math>A</math>.

Examples:

Person;                                                (* declaration only *)
Male <: Person;                                        (* subclass *)
Parent = Person & SOME hasChild . Person;              (* equivalence *)
Mother = Female & Parent;                              (* equivalence *)
ChildlessPerson = Person & ~Parent;                    (* complement *)
PersonWith3Children = EXACT 3 hasChild . Person;       (* cardinality *)
DayOfWeek = {mon, tue, wed, thu, fri, sat, sun};       (* enumeration *)

---

6. Property Declarations

Properties relate individuals to other individuals (object properties, declared in a PROP section) or to data values (data properties, declared in a DATA section).

PropDeclaration = identifier {"," identifier}
    ["[" propAttr {";" propAttr} "]"] ";".

propAttr = "DOMAIN" classExpr
         | "RANGE" classExpr
         | "INVERSE" identifier
         | "=" identifier
         | "<:" identifier
         | "CHAIN" identifier {"o" identifier}
         | characteristic.

characteristic = "FUNC" | "IFUNC" | "TRANS" | "SYM" | "ASYM" | "REFL" | "IRREFL".

DataDeclaration = identifier {"," identifier}
    ["[" dataAttr {";" dataAttr} "]"] ";".

dataAttr = "DOMAIN" classExpr
         | "RANGE" datatype
         | "<:" identifier
         | "FUNC".

Characteristics:

Keyword	Meaning	OWL Axiom
FUNC	at most one value per individual	FunctionalObjectProperty
IFUNC	at most one individual per value	InverseFunctionalObjectProperty
TRANS	transitive	TransitiveObjectProperty
SYM	symmetric	SymmetricObjectProperty
ASYM	asymmetric	AsymmetricObjectProperty
REFL	reflexive	ReflexiveObjectProperty
IRREFL	irreflexive	IrreflexiveObjectProperty

CHAIN p o q defines a property as the composition of properties <math>p</math> and <math>q</math> (a property chain). INVERSE p declares the property as the inverse of <math>p</math>. Within brackets, <: gives a super-property, and = gives an equivalent property.

Examples:

hasChild [DOMAIN Person; RANGE Person];
hasParent [INVERSE hasChild];
hasAncestor [TRANS; <: hasRelative];
hasSpouse [SYM; FUNC; DOMAIN Person; RANGE Person];
hasUncle [CHAIN hasParent o hasBrother];
hasBrother [<: hasSibling; RANGE Male];

---

7. Individual Declarations

Individuals are concrete members of classes.

IndDeclaration = identifier {"," identifier} ":" classExpr ";".

The class expression after : specifies class membership (a class assertion).

Examples:

john : Father;
mary : Female & Parent;
mon, tue, wed, thu, fri, sat, sun : DayOfWeek;

---

8. Axioms and Statements

The BEGIN ... END section contains axioms not captured by declarations. A statement is separated by ; (as a separator, not a terminator, following Wirth's convention).

statement = classExpr "<:" classExpr
          | "DISJOINT" classRef {"," classRef}
          | identifier "." identifier ":=" (identifier | literal)
          | "SAME" identifier {"," identifier}
          | "DIFF" identifier {"," identifier}.

StatementSequence = statement {";" statement}.

Form	Meaning	OWL Axiom
<math>C</math> <: <math>D</math>	every member of <math>C</math> is a member of <math>D</math>	SubClassOf (GCI)
DISJOINT <math>A, B, \ldots</math>	no individual belongs to more than one class	DisjointClasses
a.R := b	individual <math>a</math> is <math>R</math>-related to <math>b</math>	PropertyAssertion
SAME <math>a, b</math>	<math>a</math> and <math>b</math> denote the same individual	SameIndividual
DIFF <math>a, b, \ldots</math>	pairwise distinct individuals	DifferentIndividuals

The property assertion a.R := b resembles assignment in Lola but denotes a stated fact rather than a computed value. Unlike Lola, where each variable is assigned exactly once, an individual may participate in multiple property assertions for the same property (unless that property is declared FUNC).

General Concept Inclusions (GCIs) allow complex class expressions on both sides of <:, e.g., SOME hasChild . Doctor <: HappyParent — anything that has a child who is a Doctor is a HappyParent.

Examples:

DISJOINT Male, Female;
SOME hasChild . TOP <: Parent;
john.hasChild := mary;
john.hasAge := 42;
john.hasName := "John Smith";
DIFF john, mary, bob

---

9. Ontologies

An ontology is the top-level unit of description, combining declarations and axioms into a self-contained specification. The identifier at the end must match the one following ONTOLOGY.

ontology = "ONTOLOGY" identifier
    ["(" ["IMPORT" iri {"," iri}] ")"] ";"
    ["CONST" {ConstDeclaration}]
    ["CLASS" {ClassDeclaration}]
    ["PROP"  {PropDeclaration}]
    ["DATA"  {DataDeclaration}]
    ["IND"   {IndDeclaration}]
    ["BEGIN" StatementSequence]
    "END" identifier ".".

---

Complete Example

ONTOLOGY Family ();

  CONST
    MaxChildren = 20;

  CLASS
    Person;
    Male <: Person;
    Female <: Person;
    Parent = Person & SOME hasChild . Person;
    Mother = Female & Parent;
    Father = Male & Parent;
    Grandparent = Person & SOME hasChild . Parent;
    ChildlessPerson = Person & ~Parent;
    PersonWithManyChildren = Person & MIN 5 hasChild . Person;
    DayOfWeek = {mon, tue, wed, thu, fri, sat, sun};

  PROP
    hasChild [DOMAIN Person; RANGE Person];
    hasParent [INVERSE hasChild];
    hasSibling [SYM; DOMAIN Person; RANGE Person];
    hasSpouse [SYM; FUNC; DOMAIN Person; RANGE Person];
    hasAncestor [TRANS];
    hasRelative;
    hasUncle [CHAIN hasParent o hasBrother];
    hasBrother [<: hasSibling; RANGE Male];

  DATA
    hasAge [DOMAIN Person; RANGE INT; FUNC];
    hasName [DOMAIN Person; RANGE STRING];

  IND
    john : Father;
    mary : Mother;
    bob : Male;
    mon, tue, wed, thu, fri, sat, sun : DayOfWeek;

  BEGIN
    DISJOINT Male, Female;
    john.hasChild := mary;
    john.hasChild := bob;
    john.hasAge := 42;
    john.hasName := "John Smith";
    mary.hasAge := 15;
    SOME hasChild . TOP <: Parent;
    DIFF john, mary, bob
  END Family.

---

Correspondence to OWL 2 and Lola-2

Concept	Lola-2	DOLA	OWL 2 Functional Syntax
Encapsulation	MODULE	ONTOLOGY	Ontology(...)
Type/Category	TYPE	CLASS	Declaration(Class(...))
Instance	VAR	IND	Declaration(NamedIndividual(...))
Definition	:=	:= / =	EquivalentClasses / PropertyAssertion
Subsumption	—	<:	SubClassOf
And-gate / Intersection	&	&	ObjectIntersectionOf
Or-gate / Union			ObjectUnionOf
Not-gate / Complement	~	~	ObjectComplementOf
Conditional / Restriction	-> :	SOME/ONLY	ObjectSomeValuesFrom / ObjectAllValuesFrom
Array / Cardinality	[n] BIT	MIN/MAX/EXACT	ObjectMinCardinality etc.
Constructor / Enumeration	{...}	{...}	ObjectOneOf

Design notes and possible extensions

The following features are intentionally omitted from the core language for simplicity but could be added:

• Annotations (rdfs:label, rdfs:comment) — could use an @label "..." syntax after declarations.
• Data ranges — constraining datatypes, e.g., INT[>= 0, <= 150].
• Negative property assertions — e.g., john.hasChild ~:= jane.
• Prefix/namespace management — e.g., IMPORT <...> AS prefix, then prefix.ClassName.
• SWRL rules — inference rules beyond DL expressivity.
• Parameterized ontology modules — analogous to Lola's parameterized MODULE types, allowing ontology design patterns to be declared and instantiated with actual parameters.
• Disjoint union — DISJOINT UNION combining disjointness with a covering axiom.

The grammar is designed to be LL(2): a statement beginning with an identifier followed by . is a property assertion; followed by &, |, or <: it begins a class axiom. All other statement forms begin with distinct keywords.