Automatic GEneration of order-sorted first-order logical modelS

Program Input

Maude Specification

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

Test Goal

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:

Inference Rules

Activate or deactivate inference rules from Logic:

Reflexivity Rules.
Trasitivity Rules.
Congruence Rules.
Replacement Rules.

Convex Polytopic Domain


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.

SMT Solver

Choose the constraint solver:




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

How does it work

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.