1.  
  2. fbf ::= <predicato>
  3. | <negazione> | <cong> | <disg> | <implicazione>
  4. | <universale> | <esistenziale>
  5.  
  6. predicato ::= <symbol that starts with a letter>
  7. | '(' <simbolo> <termine>* ')'
  8.  
  9. negazione ::= '(' not <fbf> ')'
  10. cong ::= '(' and <fbf> <fbf> ')'
  11. disg ::= '(' or <fbf> <fbf> ')'
  12. implicazione ::= '(' ==> <fbf> <fbf> ')'
  13. universale ::= '(' forall <variabile> <fbf> ')'
  14. esistenziale ::= '(' exist <variabile> <fbf> ')'
  15. naturally you have to consider also well formed formulae which more complex:
  16. cong' ::= '(' and <fbf>* ')'
  17. disg' ::= '(' or <fbf>* ')'
  18.  
  19. termine ::= <costante> | <variabile> | <funzione>
  20. costante ::= <numeri> | <symbol that starts with a letter>
  21. variabile ::= <symbol that starts with ?>
  22. funzione ::= '(' <simbolo> <termine>* ')'