You will find the following features:

- An interactive toplevel to allow naming of objects and call to various functions.
- Solving Diophantine constraints over finite intervals
- Solving Presburger constraints
- String Rewriting Systems, KB completion.
- Term Rewrite Systems, possibly with commutative or associative-commutative symbols.
- Termination of TRSs using standard or dependency pairs criteria, automatic generation of termination orderings based on polynomial interpretations, including weak orderings for dependency pairs criteria.
- Parameterized String Rewriting Systems confluence checking
- TRS confluence checking, KB completion, modulo AC when needed

- For pentium PCs running Linux: by HTTP or by FTP
(uncompress using
`bzip2 -d ...`) - For pentium PCs running Linux, statically linked binary: by HTTP or by FTP
- For pentium PCs running MS Windows: by HTTP or by FTP
- For Mac OS X: by HTTP or by FTP

- by HTTP or by FTP.
- Also available by read-only anynomous CVS. Proceed as follows :
- Log anonymously on our CVS server by
cvs -d :pserver:guest@cvs.lri.fr:/users/demons/demons/master-sources-repository login

and leave the password empty. - check out the source tree by
cvs -d :pserver:guest@cvs.lri.fr:/users/demons/demons/master-sources-repository co cime

- the installation procedure is (see file INSTALL for more details)
cd cime autoconf ./configure make

- Later on, you may update your source tree by
cd cime cvs update -d

and recompile again

- Log anonymously on our CVS server by

More recent versions of the examples may be available in the CVS archive.

CiME> let N = parameters "N"; N : parameter_set = "N " CiME> let S = pword_signature N "s | {N>=2}; r | {N>=2}" ; S : pword_signature =CiME> let R = psrs S "s s -> | {N>=2}; s r -> r^{N-1} s | {N>=2} ; r^{N} -> | {N>=2};" ; R : S psrs = { [] s s -> | { N - 2 >= 0} ; [] s r -> ( r )^{ N - 1} s | { N - 2 >= 0} ; [] ( r )^{ N} -> | { N - 2 >= 0} ; } <3 rules> CiME> let Rnorm = psrs S "s r^{k} -> r^{N-k} s | {N>=2 /\ 1 <= k <= N-1 };"; Rnorm : S psrs = { [k ] s ( r )^{ k} -> ( r )^{ N - k} s | { (N - 2 >= 0 and k - 1 >= 0 and N - k - 1 >= 0)} ; } <1 rules> CiME> pconfluent_ext R Rnorm; Computing CP. Found 17 CP. - : bool = true

CiME> let S = word_signature "a b c"; S : word_signature =CiME> let R = SRS S " a b -> c ; b c -> a"; R : S SRS = { a b -> c, b c -> a } (2 rules) CiME> let prec = word_precedence S " a > b >c "; prec : S word_precedence = CiME> let ord = length_lex prec; ord : S word_ordering = CiME> let R' = word_completion ord R; R' : S SRS = { a b -> c, b c -> a, a^2 -> c^2, c^2 b -> a c, a c^2 -> c^2 a, a c b -> b a c } (6 rules) CiME> word_normalize R' (word S "a b c b c a b"); - : S word = a^3 c

CiME> let F = signature "0 : constant; s : unary; m,p : binary; "; F : signature CiME> let X = vars "x y z"; X : variable set CiME> let R = TRS F X " p(x,0) -> x; p(x,s(y)) -> s(p(x,y)); m(x,0) -> 0; m(x,s(y)) -> p(m(x,y),x); "; R : TRS = { p(x,0) -> x, p(x,s(y)) -> s(p(x,y)), m(x,0) -> 0, m(x,s(y)) -> p(m(x,y),x) } (4 rules) CiME> #time; time is now on CiME> termination R; Entering the termination expert. Verbose level = 0 [0] = 0; [s](X0) = 1*X0 + 1; [m](X0,X1) = 2*X0*X1 + 2*X1 + 1*X0 + 1; [p](X0,X1) = 2*X1 + 1*X0 + 1; Execution time: 0.21 sec. - : unit = () CiME>Here is a second example that uses the dependency pair termination criterion

CiME> let F = signature " 0 : constant; s : unary; minus : binary; quot : binary; "; F : signature CiME> let X =vars "x y"; X : variable set CiME> let quotient = TRS F X " minus(x,0) -> x ; minus(s(x),s(y)) -> minus(x,y) ; quot(0,s(y)) -> 0 ; quot(s(x),s(y)) -> s(quot(minus(x,y),s(y))) ; "; quotient : TRS = { minus(x,0) -> x, minus(s(x),s(y)) -> minus(x,y), quot(0,s(y)) -> 0, quot(s(x),s(y)) -> s(quot(minus(x,y),s(y))) } (4 rules) CiME> termcrit "dp"; Termination now uses dependency pair criterion - : unit = () CiME> #time on; time is now on CiME> termination quotient; Entering the termination expert. Verbose level = 0 [0] = 0; [s](X0) = 1*X0 + 1; [minus](X0,X1) = 1*X0; [quot](X0,X1) = 1*X0*X1; ['minus`](X0,X1) = 1*X0*X1; ['quot`](X0,X1) = 1*X0*X1; Termination proof found. Execution time: 1.3 sec. - : unit = () CiME>

- Since version alpha4, the Diophantine constraint solver seems to be significantly slower in some cases. Not recovered, may be it was a bug of previous versions...

20/11/2012 (formatté avec yamlpp).