FO[·]¶
Lexicon¶
(Note: The patterns below can be tested online, e.g., using pythex.org)
Token |
Pattern |
Example |
---|---|---|
ACCESSOR |
ID |
|
AND |
|
|
ANNOT |
|
|
BOOL |
|
|
CARD |
|
|
COMPARISON |
|
|
CONSTRUCTOR |
ID |
|
DATE |
|
|
DEF |
|
|
DIGIT |
|
|
EQUIVALENCE |
|
|
FORALL |
|
|
ID |
|
|
IMPLICATION |
|
|
IN |
|
|
INCLUDE |
|
|
INT |
|
|
INTEGER |
|
|
MIN |
|
|
MULT_DIV |
|
|
NAME_I |
ID or |
‘John Doe’ |
NAME_S |
ID |
|
NAME_T |
ID |
|
NAME_TH |
ID |
|
NAME_V |
ID |
|
OR |
|
|
POWER |
|
|
QUANTOR |
|
|
POINT |
|
|
R_IMPLICATION |
|
|
REAL |
|
|
REALVAL |
|
|
SUM |
|
|
SUM_MINUS |
|
|
TIMES |
|
|
TO |
|
|
UNARY |
|
|
UNIT |
|
|
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]