The DLS algorithm


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:
Atoms are:
First-order formulas are:
Second-order formulas are: 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.

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