FOL-Skolemizer

The FOL-Skolemizer converts formulas of pure first-order logic to skolemized clauses.
If you consult this page for the first time, read Syntax for the Mma-syntax and fof-example for the fof-format of TPTP-syntax.
If you use fof-format, you have to delete all line breaks within each axiom and you must use double quotation marks prior and subsequent to the fof-formula.
The FOL-Skolemizer only works for pure FOL. Do not use free variables, names, identity or mathematical functions.

Enter a logical formula:

Enter a time constraint in seconds up to 30:

If you want more detailed out insert "1":

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

The print output is:

Datenschutzerklaerung

© Timm Lampert / 2019-01-08