290 Formalization

2 Logic