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.

Use intended interpretations for _+_, _-_, _>_, _>=_ for sorts Nat (Natural numbers) and Int (Integer numbers).


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 = MROWS n = NCOLUMNS] .

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

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) and a single piece (N=1) whereas the number n_i of columns in each Ri is the dimension of vectors in the domain of sort Si. However, m and N can be specified as follows:

op P : S1 ··· Sk -> Bool [m = MROWS N = NPIECES cm = CONDMROWS] .

where MROWS, NPIECES and CONDMROWS are positive numbers.

With regards to the interpretation functions:

F1x1 + ··· + Fkxk + F0

used to interpret a function symbol:

op F : S1 ... Sk -> Sk+1 .

have a single piece (N=1). However, N can be specified as follows:

op F : S1 ··· Sk -> Sk+1 [N = NPIECES cm = CONDMROWS] .

where NPIECES and CONDMROWS are positive numbers. In functions and predicates, the last piece always corresponds to otherwise.

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.