TABLEAU-LOOPER

Introduction - Syntax - FOL-Resolver - FOL-Decider - FOL-ModelCheck - FOL-Optimizer - FOL-Skolemizer - KromHornSolver - PL-Decider - Q-Decider - Kronecker-Decider - Finitismus

The Tableau-Looper is 3-value-Decider based on clause tableaux: It returns "False" if a disproof is found and "sat" if satisfiability is proven either by a model finder or by the method of saturation. In cases, however, where the search for inference steps runs in a loop, the system returns that the proof search is terminated due to a Loop-Criterion. From this, however, it cannot be concluded that the formula is satisfiable, because proofs exist with finite numbers of loops. Further investigation has to find out.

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:

Enter a time constraint in seconds up to 300:

Datenschutzerklaerung