FO[·]¶

Lexicon¶

(Note: The patterns below can be tested online, e.g., using pythex.org)

Token	Pattern	Example
ACCESSOR	ID
AND	`&\|∧`
ANNOT	`\[[^\]]*\]`	`[This is an annotation]`
BOOL	`𝔹` or `Bool`
CARD	`#\|CARD`
COMPARISON	`=<\|≤\|<\|~=\|≠\|=\|>\|≥\|>=`
CONSTRUCTOR	ID
DATE	`#\d{4}-\d{2}-\d{2}`	`#2022-01-01`
DEF	`<-\|←`
DIGIT	`\d`
EQUIVALENCE	`<=>\|⇔`
FORALL	`[∀!]`
ID	`[^\d\W]\w*\b`	`Color`
IMPLICATION	`=>\|⇒`
IN	`in\|∈`
INCLUDE	`:⊇\|:>=`
INT	`Int\|ℤ`
INTEGER	`[+-]?\d+`	`-123`
MIN	`min\|max`
MULT_DIV	`⨯\|\*\|\/\|%`
NAME_I	ID or `'[^']*'`	‘John Doe’
NAME_S	ID
NAME_T	ID
NAME_TH	ID
NAME_V	ID
OR	`\\|\|∨`
POWER	`\^`
QUANTOR	`[∀!∃?]`
POINT	`[a-zA-Z]*\d+`	`R1`
R_IMPLICATION	`<=\|⇐`
REAL	`Real\|ℝ`
REALVAL	`[+-]?\d+(\.\d*(e[+-]?\d+))?`	`-0.01e-3`
SUM	`sum`
SUM_MINUS	`+\|-`
TIMES	`*` or `⨯`
TO	`->` or `→`
UNARY	`-\|~\|¬`
UNIT	`[^\W\d_]+(\d+\|²\|³)?`	`m2`, `m²`, `Ω`
VARIABLE	ID

Syntax¶

KnolwedgeBase ← vocabularyBlock { (VocabularyBlock | TheoryBlock | StructureBlock) };

VocabularyBlock ← 'vocabulary' [NAME_V] '{' { Declaration } '}';
  Declaration ← 'type' NAME_T [':=' TypeInterpretation] ;
    TypeInterpretation ← '{' NAME_I { ',' NAME_I } '}';
    TypeInterpretation ← 'constructed' 'from'
                         '{' ConstructorDeclaration { ',' ConstructorDeclaration } '}';
    TypeInterpretation ← '{' POINT '..' POINT '}';                          *FO[Int]
    TypeInterpretation ← REAL '[' Units ']';                                *FO[Unit]
      Units ← UNIT {UNIT} ['/' UNIT {UNIT} ];                               *FO[Unit]
      Units ← '1' '/' UNIT {UNIT};                                          *FO[Unit]
      ConstructorDeclaration ← NAME_I;
      ConstructorDeclaration ← CONSTRUCTOR '(' [ACCESSOR ':' ] Type
                               {',' [ACCESSOR ':' ] Type} ')';
        Type ← NAME_T | BOOL;
        Type ← INT | Date;                                                  *FO[Int]
        Type ← REAL;                                                        *FO[Real]
        Type ← 'Concept' '[' Signature ']';                                 *FO[Concept]
        Type ← NAME_S;                                                      *FO[PF]

  Declaration ← { ANNOT } NAME_S { ',' NAME_S } ':' Signature;
    Signature ← '(' [ Type { TIMES Type } ] ')' TO Type;
    Signature ←  Type { TIMES Type } TO Type;
  Declaration ← VARIABLE IN ( Type | Symbol );                              *FO[Sugar]
  Declaration ← 'import' NAME_V;

TheoryBlock ← 'theory' [ NAME_TH [: NAME_V] ] '{' { Assertion } '}';
  Assertion ← Interpretation;
  Assertion ← { ANNOT } '{' Rule { Rule } '}';                              *FO[ID]
    Rule ← { ANNOT } { FORALL Quantee {',' Quantee} ':' }
           Head [ DEF Expression ] '.';                                     *FO[ID]
      Head ← NAME_S '(' [ Expression {',' Expression } ] ')'
             [ '=' SumMinus ];                                              *FO[ID]

  Assertion ← Axiom;
  Axiom ← Expression '.';
  Expression ← [ { ANNOT } QUANTOR Quantee {',' Quantee} ':' ] RImplication;
      Quantee ← VARIABLE {',' VARIABLE} IN Type;
      Quantee ← VARIABLE {',' VARIABLE} [ IN Symbol ];                      *FO[Sugar]
      Quantee ← VarTuple {',' VarTuple} IN Symbol;                          *FO[Sugar]
        VarTuple ← '(' VARIABLE { ',' VARIABLE } ')';                       *FO[Sugar]
      Quantee ← VARIABLE {',' VARIABLE} IN '{' Value { ',' Value } '}';     *FO[Sugar]
      Quantee ← VarTuple {',' VarTuple} IN
                '{' TupleValue { ',' TupleValue } '}';                      *FO[Sugar]
      Quantee ← VARIABLE {',' VARIABLE} IN '{' POINT '..' POINT '}';        *FO[Int]
      RImplication ← Equivalence [R_IMPLICATION Equivalence];
      Equivalence  ← Implication [EQUIVALENCE   Implication];
      Implication  ← Disjunction [IMPLICATION   Disjunction];
      Disjunction  ← Conjunction {OR            Conjunction};
      Conjunction  ← Comparison  {AND           Comparison};
      Comparison   ← { ANNOT }
                     SumMinus    {COMPARISON    SumMinus};                  *FO[Int]
      SumMinus     ← MultDiv     {SUM_MINUS     MultDiv};                   *FO[Int]
      MultDiv      ← Power       {MULT_DIV      Power};                     *FO[Int]
      Power        ← Unary       {POWER         Unary};                     *FO[Int]
      Unary        ← { UNARY }   Enum;
      Enum         ← Base;
      Enum         ← Base IN '{' Value { ',' Value } '}';                   *FO[Sugar]
      Enum         ← NAME_S '(' Expression {',' Expression } ')'
                     'is' 'enumerated' ;                                    *FO[Sugar]
      Enum         ← Base IN '{' POINT '..' POINT '}';                      *FO[Int]

      Base ← CARD '{' Quantee {',' Quantee}  [ ':' Expression ] '}';        *FO[Agg]
      Base ← MIN '{' Expression '|' Quantee {',' Quantee}  [ ':'  Expression ] '}';*FO[Agg]
      Base ← SUM '{{' Expression '|' Quantee {',' Quantee} [ ':'  Expression ] '}}';*FO[Agg]
      Base ← 'if' Expression 'then' Expression 'else' Expression;
      Base ← { ANNOT } QUANTOR Quantee {',' Quantee} ':' RImplication;
      Base ← Symbol '(' [Expression {',' Expression}] ')';
      Base ← Identifier | VARIABLE;
      Base ← { ANNOT } '(' Expression ')';

        Symbol ← NAME_S;
        Symbol ← CONSTRUCTOR | ACCESSOR | 'is_{CONSTRUCTOR}';
        Symbol ← 'abs';                                                     *FO[Int]
        Symbol ← '$' '(' Expression ')';                                    *FO[Concept]

        Identifier ← 'true' | 'false' | NAME_I;
        Identifier ← INTEGER;                                               *FO[Int]
        Identifier ← POINT;                                                 *FO[Int]
        Identifier ← DATE | '#TODAY' ['(' INTEGER, INTEGER, INTEGER ')'];   *FO[Int]
        Identifier ← REALVAL;                                               *FO[Real]
        Identifier ← '`{NAME_S}';                                           *FO[Concept]
        Identifier ← REALVAL '[' Units ']';                                 *FO[Unit]

StructureBlock ← 'structure' [ NAME_TH [: NAME_V] ] '{' { Interpretation } '}';
  Interpretation ← NAME_T ':=' TypeInterpretation '.';
  Interpretation ← NAME_S ':=' Value '.';
  Interpretation ← NAME_S ':=' SymbolInterpretation '.';
  Interpretation ← NAME_S INCLUDE SymbolInterpretation '.';                 *FO[Sugar]
    Value ← Identifier;
    Value ← CONSTRUCTOR '(' Value {',' Value } ')';
    SymbolInterpretation ← '{' TupleValue { ',' TupleValue } '}';
    SymbolInterpretation ← '{' TupleValue TO Value { ',' TupleValue TO Value} '}' [else];
      TupleValue ← Value;
      TupleValue ← '(' Value { ',' Value } ')';
    else ← 'else' Value;                                                   *FO[Sugar]