fbf ::= | | | | | | predicato ::= | '(' * ')' negazione ::= '(' not ')' cong ::= '(' and ')' disg ::= '(' or ')' implicazione ::= '(' ==> ')' universale ::= '(' forall ')' esistenziale ::= '(' exist ')' naturally you have to consider also well formed formulae which more complex: cong' ::= '(' and * ')' disg' ::= '(' or * ')' termine ::= | | costante ::= | variabile ::= funzione ::= '(' * ')'