The following table goes through the handler code, but is not entirely exhaustive, because some of the code is confusing, redundant, or tautological.

Assumption	Free	Subexpression	Computational
Infinitesimal		any(Q.infinitesimal(arg) for arg in Mul.args)	expr.evalf() == 0 if expr.is_number
		(only works if each arg is infinitesimal or bounded)
Bounded		See truth table in AskBoundedHandler.Add
		See truth table in AskBoundedHandler.Mul	Abs()<=1**Positive -> Bounded
		Unbounded**NonZero -> Unbounded	Abs()>=1**Positive -> Bounded
		Bounded**Bounded -> Bounded
		Q.bounded(x) >> Q.bounded(log(x))
		Q.bounded(x) >> Q.bounded(exp(x))
		(these last two may be iff)
Commutative		Not commutative if any subexpression is not commutative
		(it actually just checks the .args, but I think forward
		chaining would give this)
Square			expr.shape[0] == expr.shape[1]
Symmetric		all(symmetric(arg) for arg in MatMul.args)
		A*…*A.T is symmetric iff the … is symmetric
		all(symmetric(arg) for arg in MatAdd.args)
	~Q.square >> ~Q.symmetric	symmetric iff square for ZeroMatrix
	(this is only specified for	Q.symmetric(A) iff Q.symmetric(A.T)
	MatrixSymbol, but it should	slice is symmetric if it’s on_diag and the parent is
	be true for any expression)	symmetric
Invertible	Q.invertible >> Q.square	Mul is invertible iff each arg is	(this is not in there, but for an
		Identity and Inverse are always invertible	explicit matrix, the invertibility
		ZeroMatrix is always not invertible	can be computed)
		(not in there, but Q.invertible(A) iff Q.zero(det(A)))
		A is invertible iff A.T is invertible
		slice is invertible if it’s on_diag and the parent is
		invertible
Orthogonal	Q.orthogonal >> Q.invertible	MatMul is orthogonal iff each factor is and the scalar
	Q.orthogonal >> Q.square	factor is 1
	(this can be deduced)	MatMul is not orthogonal if any factor is not invertible
		(this one can probably be deduced from other facts)
		Identity is always orthogonal
		ZeroMatrix is never orthogonal
		A is orthogonal iff A.T is orthogonal
		A is orthogonal iff A**-1 is orthogonal
(I skipped a
lot of the
matrix
expression
stuff because
it was
getting
repetitive)
Prime		Mul of integers is not prime (note, this is not entirely	For explicit integers, uses isprime
		true, as Q.integer does not mean it’s not 1)
		integer**integer is not prime (again, not true because
		of some corner cases)
Composite	composite iff nonprime
	positive integer
Even	even >> integer	Various combinations of even and odd in Mul	For explicit integers i % 2 == 0
	various things that can be	Integer*Integer is even if Integer + Integer is odd
	deduced from this	If exactly one element of a Mul is irrational, it isn’t
		even (actually isn’t an integer, so it probably should
		go there).
		The obvious ones for even and odd in Add
		Various rules for integer**integer
		if x is even, then abs(x), re(x), im(x) are even
Odd	odd iff integer and not even
Negative		positive + positive = positive	If is_number, evalf < 0
		negative + negative = negative
		(this is actually done more generally for and Add of n
		args)
		For Mul, parity of positive and negative elements
		real**even = nonnegative
		real**odd = same as base
		nonnegative**positive = nonnegative
		exp(x) is positive if x is real (should follow from Pow
		but exp is not a Pow)
NonZero		Add is nonzero if all terms are positive or if all terms	expr.evalf() != 0
		are negative
		Mul is nonzero iff each term is nonzero
		Pow is nonzero if base is nonzero (reverse implication
		is true only for positive exponent)
		Abs(x) is zero iff x is zero
Zero	zero iff not nonzero and	Mul is zero iff any term is zero. Should be deducible
	real	from nonzero (or visa-versa)
positive		If each term in a Mul is positive or negative, it is	expr is real and expr.evalf() > 0
		positive if there are an even number of negative terms
		Add is positive if at least one positive term and the
		rest are nonnegative
		positive**real = positive
		negative**even = positive
		negative**odd = not positive
		exp(real) = positive
		factorial(integer) = positive
		abs(nonzero) = positive (note, this really should be
		not zero, not nonzero, because it is true even for
		complex non-zero numbers).
		Trace(positive_definite) = positive
		Determinant(positive_definite) = positive
		MatrixElement on the diagonal is positive if the matrix
		is positive_definite
Integer		Integer + Integer = Integer	int(expr.round()) == expr
		Integer + not Integer = not Integer	Rational (the class) == not Integer
		Integer*Integer = Integer	(otherwise it would evaluate to
		Integer*Irrational = not Integer (in general, if there is	Integer)
		exactly one irrational, it is irrational)
		odd/even = not integer
		Abs(x) is integer iff x is integer (not correct; only
		true if x is also real)
		MatrixElement is integer if the Matrix is IntegerElements
		Same with Determinant and Trace
Rational		Rational + Rational = Rational
		Rational + not rational = not rational (in general, if
		exactly one non-rational, it is not rational)
		Same for Mul

• It’s hard to tell which implications are really double implications. Each one would have to be checked.
• There are a lot “if Q.assumption(expr) in conjuncts(assumptions)” which are completely irrelevant to the handler in question. I have a hard time believing that these wouldn’t work without this bit of code.
• Some of these apply to single constants (like pi), which could technically be viewed as subexpression or computational
• I don’t think there’s a need to special-case things like “IdentityMatrix is always invertible” in the code. You can just add the fact Equivalent(Q.invertible(A), True) when A is an IdentityMatrix, and it will take care of itself. This may sound silly, but I think we can use the same idea for the computational assumptions.
• I’m not sure how the Factorization stuff in the matrix expressions work.
• Most subexpressions are just vectorized over the same assumption, either via And or Or. A few are interesting, though. For example integer*integer is even if integer + integer is odd.
• The current handlers code is just terrible. Half the time it uses the new assumptions, half the time it uses things like “if not as_real_imag()[1]” (instead of Q.real). There are a ton of unnecessary redundancies (not just logically duplicate, but actually duplicate in that the current code would still compute the same thing if certain lines of code were removed, such as many duplicate “if self._number()” calls). Some of the logic is wrong (I’ve pointed out some instances of this above). In many places, the fuzzyness of the logic is not taken into account. In those places that do, some use fuzzy_or and so on, and some write the difficult to read for loop. The few handlers that are documented have confusing docstrings, which mention restricted cases of what is actually implemented, or even cases that aren’t even relevant to the particular assumption at hand (though to be sure, the truth tables for the bounded assumption are quite helpful). Some functions are implemented, but seemingly at random. The code is hard to read, mostly because most of it feels duplicated, but also because it can be hard to convert loops and if blocks to three-valued fuzzy logic.