FOL-ModelCheck

FOL-ModelChecker

Introduction - Syntax - Tableau-Looper - FOL-Resolver - FOL-Decider - FOL-Optimizer - KromHornSolver - PL-Decider - Q-Decider - Kronecker-Decider - Finitismus

The FOL-ModelChecker returns a model if there is any.
In the case of infinite models, a finite series of finite "transcendent" models is returned that converges to an infinite model as its limit by increasing the upper bound of the domain just as a series of decimal or rational numbers converges to a number as its limit.
I call a finite model "transcendent" if its interpretations of predicates refer to some object that is not part of the finite domain of that model. In fact, this "transcendent object" will be a natural number i+1 and the finite domain of the model the series of natural numbers 1 to i.
Since the FOL-ModelChecker is based on the FOL-Decider, it may happen that a an infinite model is indicated although the formula is not satisfiable. Therefore, this tool is not quite correct. Yet, this won't happen with time limit <100 seconds.

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 number as upperbound for the domain:

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

Enter a time constraint in seconds up to 300:

You may try other forms of presentation of models by entering "0" or "1":
Modellevel 0 provides a model that also includes tuples satisfying negated predicates that are neccessary part of the returned model.
Modellevel 1 provides even more detailed distinctions within a model by separating neccessary, optional and free features of interpretations.

In case no modellevel or modellevel 0 is chosen, "D" abbreviates "domain" and interpretations are presented as tables omitting brackets of sets. "" indicates the empty set.

result

Datenschutzerklaerung