FOL-Decider

The FOL-Decider decides formulas of pure FOL by an exhaustive proof search in the NNF-calculus, cf. FOL-Decider, pp. 1-43.
Yet, it is not quite correct because it may discard proofs (cf. the comment to Theorem 6.16).

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:

A[x,E[y,A[z,F[x,y]&&(Implies[F[z,x],F[z,y]])&&!F[x,x]]]]

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

Enter a time constraint in seconds up to 300:

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

The print output is:

Datenschutzerklaerung

© Timm Lampert / 2022-05-05