fbf ::= <predicato>
| <negazione> | <cong> | <disg> | <implicazione>
| <universale> | <esistenziale>
predicato ::= <simbolo che comincia con una lettera>
| '(' <simbolo> <termine>* ')'
negazione ::= '(' not <fbf> ')'
cong ::= '(' and <fbf> <fbf> ')'
disg ::= '(' or <fbf> <fbf> ')'
implicazione ::= '(' ==> <fbf> <fbf> ')'
universale ::= '(' forall <variabile> <fbf> ')'
esistenziale ::= '(' exist <variabile> <fbf> ')'

Naturally well formed formulae (FBF) more complex have to be considered
cong' ::= '(' and <fbf>* ')'
disg' ::= '(' or <fbf>* ')'

termine ::= <costante> | <variabile> | <funzione>
costante ::= <numeri> | <simboli che cominciano con una lettera>
variabile ::= <simboli che cominciano con ?>
funzione ::= '(' <simbolo> <termine>* ')'