[Logic] Add conversion function for logic formulas to existential disjunctive normal form

[elvilio]

Convert all logic formulas to normal form that uses only existentials and disjunctions following using the equivalences:

• (p or q) t == (p t) or (q * t)
• (exists x. p) q == exists x. (pq) where (x is not in the free variables of q)
• equivalences of the first order logic

Note that the existential quantification is external with respect to the disjoints.

[Yurand2000]

TO DO:

• [ ] More tests
• [ ] Tests: Translate formulas from data structure style to real code style (which will be parsed), for better readability.