Generalized quantifiers in Lark grammar

20 views Asked by At

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?

0

There are 0 answers