# AGES

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.

### Predicates

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.

### Timeout

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:

## AGES

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.

## Online examples

In order to test the tool, we provide several 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.