Attention,

l'unité Logic de Maple 2016 fait des erreurs graves. Nous avons détecté par exemple que le fait d'utiliser des variables indicées comme X[0],X[1],X[2] donne de faux résultats. Il semble suffire de les renommer en X0,X1,X2 avec par exemple

Code maple : Sélectionner tout - Visualiser dans une fenêtre à part
1
2
3
X:=proc(i) local s;
s:=cat("X",i);
convert(s,symbol);end:

ainsi X(78) donnera X78.

un exemple d'erreur : on demande des conditions et en plus à ce que (X[0]orX[1]orX[2]). Donc au moins une des trois variables doit être à vrai.

a) avec des variables indicées :
Code maple : Sélectionner tout - Visualiser dans une fenêtre à part
1
2
f=(((X[1]andX[0])or(X[2]andX[0]))or((X[0]andX[0])or(X[2]andX[2])))and(X[0]orX[1]orX[2]) 
Satisfy(f) donne un résultat faux : {X[0] = false, X[1] = false, X[2] = false}

b) avec des variables symbolisées par notre procédure "X" :
Code maple : Sélectionner tout - Visualiser dans une fenêtre à part
1
2
f=(((X1andX0)or(X2andX0))or((X0andX0)or(X2andX2)))and(X0orX1orX2)
Satisfy(f) donne un résultat qui semble correct : {X0 = false, X1 = false, X2 = true}

un autre exemple du même type :

Code maple : Sélectionner tout - Visualiser dans une fenêtre à part
1
2
(((X[1]andX[0])or(X[0]andX[1]))or((X[1]andX[2])orX[0]))and(X[0]orX[1]orX[2])   ---> {X[0] = false, X[1] = false, X[2] = false}
(((X1andX0)or(X0andX1))or((X1andX2)orX0))and(X0orX1orX2)                            ---> {X0 = false, X1 = true, X2 = true}


MapleSoft sont chers mais pas très bons quand même. ZUT !