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