Automatic GEneration of order-sorted first-order logical modelS
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.
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:
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 = 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.
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 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.