The FOL-optimizer converts pure FOL-formulas to a minimized disjunction of conjunctions of anti-prenex formulas, cf. Minimizing Disjunctive Normal Forms of Pure First-Order Logic, Logic Journal of the IGPL 25.3 (2017), pp. 325-347.
If you consult this page for the first time, read Syntax. Do not use free variables, names, identity or mathematical functions.© Timm Lampert / 2018-04-09