Here is the Lark grammar I created for parsing logical statements:
Lark('''
RELATION: CNAME
%import common.CNAME
?logical_implication: logical_operator
| logical_implication "->" logical_operator -> implication
?logical_operator: special_operator
| logical_operator "and" special_operator -> conjunction
| logical_operator "or" special_operator -> disjunction
| logical_operator "==" special_operator -> equal
| logical_operator "!=" special_operator -> not_equal
| logical_operator ">" special_operator -> greater_than
| logical_operator "<" special_operator -> lower_than
| logical_operator ">=" special_operator -> greater_equal
| logical_operator "<=" special_operator -> lower_equal
?special_operator: properties
| "not" logical_operator -> negation
| product "is" properties -> is
| product "is not" properties -> is_not
?properties: product
| "total_order" -> total_order
| "transitive" -> transitive
| "reflexive" -> reflexive
| "symmetric" -> symmetric
| "asymmetric" -> asymmetric
| "antisymmetric" -> antisymmetric
?product: atom
| "\i{" product "}" -> inverse
| product "°" atom -> composition
| product "&" atom -> intersection
| product "|" atom -> union
| product "-" atom -> difference
| product "^" atom -> symmetric_difference
| "\c{" product "}" -> complement
?atom: "("logical_implication")"
| RELATION
%import common.WS
%ignore WS
''', start='logical_implication')
Here is an example statement:
statement = "R is reflexive -> R | S is symmetric"
I want to add generalized quantifiers \forall and \forallrelations to my statements:
statement = "\forall{A} \forallrelations{R}{A} \forallrelations{R}{B} (R is reflexive -> R | S is symmetric"
\forallrelations{R}{A} stands for ∀R ⊆ A ⨯ A
I haven't managed to find out how to include such generalized quantifiers in Lark's grammar. Does anyone have an idea?