z3 - Questions about using Z3Py online to apply the Routh-Hurwitz Theorem -
example 1:
we apply rh theorem using following code
k = real('k') print simplify(and(12 - 3*k >0 , 20 + 0.25*k >0)) and output is:
¬(k ≥ 4) ∧ ¬(k ≤ -80) example 2:
we apply rh theorem using following code
k, a1, a2, a3 = reals('k a1 a2 a3') a1 = 20 + 1.5*k a2 = 4 a3 = 4*k -100 print simplify(and(a1 > 0 , a3 > 0, a1*a2 > a3)) and output is
¬(k ≤ -40/3) ∧ ¬(k ≤ 25) ∧ ¬(k ≤ -90) example 3:
we apply rh theorem using following code
k = real('k') a1 = 10 a2 = 30 - 2.4*k a3 = 2 a4 = 100 + 5*k print simplify(and(a4 > 0, a1*a2*a3 > a3**2 + a4*a1**2)) and output is
¬(k ≤ -20) ∧ ¬(k ≥ -2351/137) example 4:
we apply rh theorem using following code
u, s, d, g, n, b , = reals('u s d g n b a') c1 = 2*u + s + d + g prove(implies(and(u > 0, s > 0, d >0, g >0), c1 > 0)) c2 = u*g + u**2 + s*u + 2*d*u + s*d + s*g + d*g c3 = d*u**2 - n*a*b*s + d*u*g + s*d*u + s*d*g prove(implies(and(u > 0, s > 0, d >0, g >0, >0, b > 0, n >0), c1*c2 > c3)) and output is:
proved proved the remanent rh condition : c3 > 0 leads to
example 5:
we apply rh theorem using following code
u, s1, s2, d, g, n, b , = reals('u s1 s2 d g n b a') c1 = d + 3*u + s1 + g + s2 prove(implies(and(u > 0, s1 > 0, s2 > 0, d >0, g >0), c1 > 0)) c2 = s2*g + 3*d*u + d*g + d*s1+ s1*s2 + 3*u**2 + 2*s2*u + 2*s1*u+ s1*g + 2*u*g + d*s2 c3 = 2*d*u*g + s1*u*g + 2*d*s2*u + 3*d*u**2 + d*g*s1 + s1*s2*g + u**3 + u*s2*g + 2*d*s1*u + s1*s2*u + g*u**2 + d*g*s2 + s1*u**2 + d*s1*s2 + s2*u**2 prove(implies(and(u > 0, s1 > 0, s2 >0, d >0, g >0, >0, b > 0, n >0), c3 > 0)) c4 = d*g*u**2 + d*s2*u**2 + s1*d*u*g + s1*d*s2*u + s1*d*s2*g - n*a*b*s1*s2 + d*u**3 + s1*d*u**2 + d*u*s2*g prove(implies(and(u > 0, s1 > 0, s2 >0, d >0, g >0, >0, b > 0, n >0), c1*c2*c3 > c3**2 + c4*c1**2)) and output is:
proved proved proved it can try online here.
the remanent rh condition : c4 > 0 leads to
questions:
please let me know if know more efficient code kind of problems
how simplify outputs examples 1, 2 , 3.
for exampple 4, how solve c3 > 0 respect b using z3py , obtain formula ro
for exampple 5, how solve c4 > 0 respect b using z3py , obtain formula ro
many thanks.
Comments
Post a Comment