Automatic Generation of Logical Models with AGES

We describe a new tool, AGES, which can be used to automatically generate models for order-sorted first-order theories. The tool uses linear algebra techniques to associate finite or infinite domains to the different sorts. Function and predicate symbols are then interpreted by means of piecewise interpretations with matrix-based expressions and inequalities. Relations interpreting binary predicates can be specified to be well-founded as an additional requirement for the generation of the model. The system is available as a web application.