# 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