This is a demonstration of an automatic configuration system derived from an IDP theory. Put a file with a vocabulary V, theory T and structure S in the theory tab. All symbols (except for the ones starting with an underscore) will subsequently come available in the interface as an interactive configuration problem.

Every field in the form is accompanied by a "+" and "-"-button. Selecting the "+" means that element will be part of the interpretation of the symbol. Selecting "-" means that the element won't be part of the interpreation of a symbol. IDP will ensure that your selection remains valid and automatically derive extra facts for you that follow from the theory.

There are two ways for completing your selection to a full model. "Expand to model" expands your selection to a full model based on your current selection. If there are any terms defined you can also find a model which is minimal for that term with the "Minimize" button.

More information about IDP can be found here