FO[ID]

Goal

The goal of FO[ID] is to allow defining concepts in terms of other concepts, in a modular way. The definition can be inductive. ID stands for “Inductive Definition”.

Lexicon

Token

Pattern

Example

DEF

<-|←

FORALL

[∀!]

Syntax

FO[ID] adds these production rules:

  Assertion ← { ANNOT } '{' Rule { Rule } '}';
    Rule ← { ANNOT } { FORALL Quantee {',' Quantee} ':' }
           Head [ DEF Expression ] '.';
      Head ← NAME_S '(' [ Expression {',' Expression } ] ')'
           [ '=' SumMinus ];
flowchart LR subgraph Assertion direction LR start{ } --> ANNOT([ANNOT]); ANNOT --> ANNOT; start --> lp["'{'"]; ANNOT --> lp; lp --> Rule([Rule]); Rule --> dot["'.'"]; dot --> Rule dot --> rp["'}'"]; end;
flowchart LR subgraph "Rule" direction LR start{ } --> ANNOT([ANNOT]); ANNOT --> ANNOT; start --> FORALL[FORALL]; ANNOT --> FORALL; FORALL --> Quantee([Quantee]); Quantee --> comma["','"]; comma --> Quantee2([Quantee]); Quantee2 --> comma; Quantee --> colon["':'"]; Quantee2 --> colon; colon --> Head([Head]); ANNOT --> Head; Head --> DEF[DEF]; DEF --> Expression3([Expression]); Expression3 --> END{ }; Head --> END; start --> Head; end;
flowchart LR subgraph "Head" direction LR NAME_S([NAME_S]) --> lp2["'('"]; lp2 --> rp2["')'"]; lp2 --> Expression([Expression]); Expression --> rp2; Expression --> comma2["','"]; comma2 --> Expression2([Expression]); Expression2 --> comma2; Expression2 --> rp2; rp2 --> eq["'='"]; eq --> SumMinus([SumMinus]); rp2 --> END{ }; SumMinus --> END; end;

Well-formedness

  1. The Variable occurring in a rule must be in the scope of a quantifier that declares it. The scope of the quantifiers in the head of a Rule is the whole rule.

  2. NAME_S must have been declared in the vocabulary.

  3. The number and types of Expression applied to NAME_S must match its type signature.

  4. The = sign must occur in rule where NAME_S has been declared as a non-boolean function. The type of the Expression after = must be the same as the type of NAME_S.

  5. The Expression after DEF must be boolean.

Semantics

An inductive definition specifies a unique interpretation for a predicate (or function) symbol, given the interpretation of its parameters. The parameters of a definition are the symbols that occur in it (by contrast, the tuple of arguments are the values applied to its symbol).

The semantics of a predicate definition is the well-founded semantics [Den00]. When the predicate is well-defined, i.e., the definition is not a paradox like { p() ← ¬p(). }, the definition can be seen as the description of a constructive process. The construction process starts with an empty relation, i.e., the predicate is false for any tuple of values. Whenever the body of a rule (i.e. the Expression after DEF) is true, the tuple of values in the header is added to the relation. The process continues until a fix point is reached, i.e., no tuple of values can be added to the relation.

The construction process is similar for a function. The process starts with the function being undefined for every tuple of arguments. Whenever the body of a rule is true, the mapping of tuple of arguments to a value described in the header is added to the function interpretation. The process continues until a fix point is reached, i.e., no mapping can be added to the function interpretation.

The knowledge engineer should make sure that a defined function is defined over its whole domain, i.e., that the rules are such that the function is defined for every tuple of arguments in its domain, and for any interpretation of the parameters of the definition. He should also make sure that the rules of a function definition are not conflicting. Conflicting rules specify 2 different values for the same tuple of arguments. A reasoning engine may help him satisfy these requirements.

Examples

    [Definition of convex]
    { convex() ← [All angles are below 180°]
                 ∀n ∈ Side_Nr: angle(n)<180. }

angle is a parameter of the definition of convex. convex is a nullary predicate: it does not take any argument.

FO(ID) abstract language

The formal semantics of FO(ID) is described in [Den00]. FO(ID) can be reduced to FO by a process described in [PT05].