FOL-Optimizer

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.

Enter a logical formula:

E[y[2], E[y[1], f[y[2], y[1]]] && A[x[1], E[y[3], f[y[3], x[1]]] || f[y[2], x[1]]]]

Your input in TraditionalForm (including quantifier definitions and omitted →, ≡, ⊽, ⊼, ⊻):

Enter a time constraint in seconds up to 500:

The result is ({time in seconds, result}):

$(\left[\right])$

Datenschutzerklaerung

© Timm Lampert / 2018-04-09