FOL-RESOLVER


The FOL-Resolver is 3-value-Decider based on resolution: 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:

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

The print output is:

   
  
  
  


Powered by webMathematica

Datenschutzerklaerung

© Timm Lampert / 2022-05-05