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

OWL version of Family example

Here is the complete OWL 2 Functional Syntax equivalent of the DOLA `Family` example, ready for copy-paste:

```owl
Prefix(:=<http://example.org/family#>)
Prefix(owl:=<http://www.w3.org/2002/07/owl#>)
Prefix(rdf:=<http://www.w3.org/1999/02/22-rdf-syntax-ns#>)
Prefix(xml:=<http://www.w3.org/XML/1998/namespace>)
Prefix(xsd:=<http://www.w3.org/2001/XMLSchema#>)
Prefix(rdfs:=<http://www.w3.org/2000/01/rdf-schema#>)

Ontology(<http://example.org/family>

  ##
  ## Class Declarations
  ##

  Declaration(Class(:Person))
  Declaration(Class(:Male))
  Declaration(Class(:Female))
  Declaration(Class(:Parent))
  Declaration(Class(:Mother))
  Declaration(Class(:Father))
  Declaration(Class(:Grandparent))
  Declaration(Class(:ChildlessPerson))
  Declaration(Class(:PersonWithManyChildren))
  Declaration(Class(:DayOfWeek))

  ## Male <: Person
  SubClassOf(:Male :Person)

  ## Female <: Person
  SubClassOf(:Female :Person)

  ## Parent = Person & SOME hasChild . Person
  EquivalentClasses(:Parent
    ObjectIntersectionOf(:Person
      ObjectSomeValuesFrom(:hasChild :Person)))

  ## Mother = Female & Parent
  EquivalentClasses(:Mother
    ObjectIntersectionOf(:Female :Parent))

  ## Father = Male & Parent
  EquivalentClasses(:Father
    ObjectIntersectionOf(:Male :Parent))

  ## Grandparent = Person & SOME hasChild . Parent
  EquivalentClasses(:Grandparent
    ObjectIntersectionOf(:Person
      ObjectSomeValuesFrom(:hasChild :Parent)))

  ## ChildlessPerson = Person & ~Parent
  EquivalentClasses(:ChildlessPerson
    ObjectIntersectionOf(:Person
      ObjectComplementOf(:Parent)))

  ## PersonWithManyChildren = Person & MIN 5 hasChild . Person
  EquivalentClasses(:PersonWithManyChildren
    ObjectIntersectionOf(:Person
      ObjectMinCardinality(5 :hasChild :Person)))

  ## DayOfWeek = {mon, tue, wed, thu, fri, sat, sun}
  EquivalentClasses(:DayOfWeek
    ObjectOneOf(:mon :tue :wed :thu :fri :sat :sun))

  ##
  ## Object Property Declarations
  ##

  Declaration(ObjectProperty(:hasChild))
  Declaration(ObjectProperty(:hasParent))
  Declaration(ObjectProperty(:hasSibling))
  Declaration(ObjectProperty(:hasSpouse))
  Declaration(ObjectProperty(:hasAncestor))
  Declaration(ObjectProperty(:hasRelative))
  Declaration(ObjectProperty(:hasUncle))
  Declaration(ObjectProperty(:hasBrother))

  ## hasChild [DOMAIN Person; RANGE Person]
  ObjectPropertyDomain(:hasChild :Person)
  ObjectPropertyRange(:hasChild :Person)

  ## hasParent [INVERSE hasChild]
  InverseObjectProperties(:hasParent :hasChild)

  ## hasSibling [SYM; DOMAIN Person; RANGE Person]
  SymmetricObjectProperty(:hasSibling)
  ObjectPropertyDomain(:hasSibling :Person)
  ObjectPropertyRange(:hasSibling :Person)

  ## hasSpouse [SYM; FUNC; DOMAIN Person; RANGE Person]
  SymmetricObjectProperty(:hasSpouse)
  FunctionalObjectProperty(:hasSpouse)
  ObjectPropertyDomain(:hasSpouse :Person)
  ObjectPropertyRange(:hasSpouse :Person)

  ## hasAncestor [TRANS]
  TransitiveObjectProperty(:hasAncestor)

  ## hasUncle [CHAIN hasParent o hasBrother]
  SubObjectPropertyOf(
    ObjectPropertyChain(:hasParent :hasBrother)
    :hasUncle)

  ## hasBrother [<: hasSibling; RANGE Male]
  SubObjectPropertyOf(:hasBrother :hasSibling)
  ObjectPropertyRange(:hasBrother :Male)

  ##
  ## Data Property Declarations
  ##

  Declaration(DataProperty(:hasAge))
  Declaration(DataProperty(:hasName))

  ## hasAge [DOMAIN Person; RANGE INT; FUNC]
  DataPropertyDomain(:hasAge :Person)
  DataPropertyRange(:hasAge xsd:integer)
  FunctionalDataProperty(:hasAge)

  ## hasName [DOMAIN Person; RANGE STRING]
  DataPropertyDomain(:hasName :Person)
  DataPropertyRange(:hasName xsd:string)

  ##
  ## Individual Declarations
  ##

  Declaration(NamedIndividual(:john))
  Declaration(NamedIndividual(:mary))
  Declaration(NamedIndividual(:bob))
  Declaration(NamedIndividual(:mon))
  Declaration(NamedIndividual(:tue))
  Declaration(NamedIndividual(:wed))
  Declaration(NamedIndividual(:thu))
  Declaration(NamedIndividual(:fri))
  Declaration(NamedIndividual(:sat))
  Declaration(NamedIndividual(:sun))

  ## john : Father
  ClassAssertion(:Father :john)

  ## mary : Mother
  ClassAssertion(:Mother :mary)

  ## bob : Male
  ClassAssertion(:Male :bob)

  ## mon, tue, wed, thu, fri, sat, sun : DayOfWeek
  ClassAssertion(:DayOfWeek :mon)
  ClassAssertion(:DayOfWeek :tue)
  ClassAssertion(:DayOfWeek :wed)
  ClassAssertion(:DayOfWeek :thu)
  ClassAssertion(:DayOfWeek :fri)
  ClassAssertion(:DayOfWeek :sat)
  ClassAssertion(:DayOfWeek :sun)

  ##
  ## Axioms (BEGIN ... END)
  ##

  ## DISJOINT Male, Female
  DisjointClasses(:Male :Female)

  ## john.hasChild := mary
  ObjectPropertyAssertion(:hasChild :john :mary)

  ## john.hasChild := bob
  ObjectPropertyAssertion(:hasChild :john :bob)

  ## john.hasAge := 42
  DataPropertyAssertion(:hasAge :john "42"^^xsd:integer)

  ## john.hasName := "John Smith"
  DataPropertyAssertion(:hasName :john "John Smith"^^xsd:string)

  ## mary.hasAge := 15
  DataPropertyAssertion(:hasAge :mary "15"^^xsd:integer)

  ## SOME hasChild . TOP <: Parent
  SubClassOf(
    ObjectSomeValuesFrom(:hasChild owl:Thing)
    :Parent)

  ## DIFF john, mary, bob
  DifferentIndividuals(:john :mary :bob)

• • Note:** The DOLA `CONST MaxChildren = 20` has no OWL counterpart — it is a purely syntactic convenience for use inside DOLA cardinality expressions and produces no axiom. The ## comments above each axiom show the corresponding DOLA source line.<

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.