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.
© Timm Lampert / 201-01-08