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.
Select the interpretation for the -> predicate:
Select the interpretation for the ->* predicate:
Activate or deactivate inference rules from Logic:
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.