FO[·]

Lexicon

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

Token

Pattern

Example

ACCESSOR

ID

AGG

sum|min|max

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

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_MINUS

+|-

TIMES

* or

TO

-> or

UNARY

-|~|¬

UNIT

[^\W\d_]+(\d+|²|³)?

m2, , Ω

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;
  Declaration ← { ANNOT } 'partial' NAME_S { ',' NAME_S } ':' Signature;    *FO[PF]
    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 ← AGG '(' 'lambda' 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]
        Symbol ← 'dom' '(' Expression ')';                                  *FO[PF]

        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]
  Interpretation ← 'dom' '(' NAME_S ')' ':=' SymbolInterpretation '}' '.';  *FO[PF]
    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]