# The DLS algorithm

## Syntax

A *name* is a string of alphanumeric characters (`exists`

and `all`

are reserved words and should not be used). A *predicate-name* is a name beginning with a capital letter.

*Terms* are:
- Constants. A name without capital letters.
- Variables. A name without capital letters.
- Functions. A name without capital letters, followed by parentheses containing one or more terms
separated by commas.

*Atoms* are:
- Predicates. A predicate-name, followed by parentheses containing one or more terms separated by commas.
- Equality statements.
* term=term*.

*First-order formulas* are:
- Atoms are formulas.
- If
`A`

is a formula then `-A`

is a formula.
- If
`A`

is a formula then `(A)`

is a formula.
- If
`A1`

, ... ,`An`

are formulas then `A1&`

... `&An`

is a formula.
- If
`A1`

, ... ,`An`

are formulas then `A1|`

... `|An`

(or `A1#`

... `#An`

)is a formula.
- If
`A`

and `B`

are formulas then `A->B`

is a formula.
- If
`A`

and `B`

are formulas then `A<->B`

is a formula.
- If
`x1`

, ... ,`xn`

are variables and `A`

is a formula then `all x1 x2`

... `xn A`

is a formula.
- If
`x1`

, ... ,`xn`

are variables and `A`

is a formula then `exists x1 x2`

... `xn A`

is a formula.

*Second-order formulas* are:
- First-order formulas.
- If
`A`

is a first- or second-order formula and X is a predicate-name then `all X (A)`

is a second-order formula.
- If
`A`

is a first- or second-order formula and X is a predicate-name then `exists X (A)`

is a second-order formula.

Note that we do not allow multiple predicate-names after a second-order quantifier. (Example. ` all P Q R`

have to be written `all P all Q all R `

)

*Nested abnormality theories*
The syntax of a block is {*Predicate-list* : *Formula-Block-list*} where *Predicate-list*
is a list of zero or more predictes that occur in the formulas, the predicates are separated with commas.*
Formula-Block-list* is one ore more formulae or blocks separated with commas.

White space (space, tabs and newlines) will be ignored except when separating the variables in a quantifier
expression.
The operators with the highest precedence are -, `all`

,`exists`

and parentheses, and in
receding order &, #, -> and finally <-> with lowest precedence. Right associativity is assumed.

EXAMPLES

`P(a) & P(b) & P(c) `

`all a b exists c (P(a) & P(b) -> Q(c))`

`all x1 x2 y1 y2 (FeatureColor(paint(x1,y1),state) & FeatureColor(paint(x2,y2),state)-> x1=x2 & -y1=y2)`

More examples will be added later.

dls | Circumscription | Main page