**A**utomatic **GE**neration of order-sorted first-order
logical model**S**

Select a file to upload, or paste your code un the following text area:

Write the test goal in the next text field

Use a new line to separate each goal.

Select the interpretation for the -> predicate:

Select the interpretation for the ->* predicate:

Activate or deactivate inference rules from Logic:

Reflexivity Rules.

Trasitivity Rules.

Congruence Rules.

Replacement Rules.

Value for m:

Value for n:

Select timeout in seconds (1 <= timeout <= 300):

m and n are the number of rows and columns (respectively) of the matrix defining the convex polytopic domain, see here.

Consequently, the domain associated to a sort s is a subset of R^n. Each sort S can be given with its own m and n in the specification as follows:

`sort S [m = M n = N] .`

where M and N are positive numbers. If m or n is missing in the sort declaration, the general value given in AGES' text boxes is taken.

Furthermore, by default matrices Ri used in the inequality:

`R1x1 + ··· + Rkxk + R0 >= 0`

used to interpret a predicate:

`op P : S1 ... Sk -> Bool .`

have a single row (m=1) whereas the number n_i of columns in each Ri is the dimension of vectors in the domain of sort Si. However, m can be specified as follows:

`op P : S1 ··· Sk -> Bool [m = M] .`

where M is a positive number.

Choose the constraint solver:

Is a tool for generate logical models, for use with Order-Sorted First Order Logic.

This tool is completely coded in Haskell using MU-TERM as programming framework for developing. This tool generates models using polynomial, convex domains, and convex matrix interpretations, to test new theories in automatic verification.

In order to test the tool, we provide 2 examples to show the syntax of the MAUDE program and the goal to verify. Click on the name of the example to load it into the input data section.

- Manna and Pnueli summation example (positiveness)
- Manna and Pnueli factorial example (positiveness)
- Sorted Toyama example (termination)
- Order-Sorted Specification with replacement restrictions (termination)
- Conditional rules example (convex domain)
- Conditional rules example v2 (convex domain)
- Toyama example (piecewise interpretation)
- Toyama example v2 (piecewise interpretation)
- Zantema example (piecewise interpretation)
- Implies example (operational termination)