is(k::OrProp(even, odd)) assuming k::integer;
                             false

is(k::Or(posint, nonposint)) assuming k::integer; # a synonym for OrProp
                             false

is(`or`(k::posint, k::negint, k = 0)) assuming k::integer;
                             false

Not including the infix or because that would fail for k=0 for different reasons.

1.

eliminate({-a+x+y+z, -b+x*y+y*z+x*z, -c+x*y*z, -P+x^4+y^4+z^4}, {x, y, z});
    [{x = (sqrt(c^2*(a^2*b^2-2*a*b*c-4*b^3+c^2)/b^4)*b^2+a*b*c-c^2)/(2*b*c),
      y = -(sqrt(c^2*(a^2*b^2-2*a*b*c-4*b^3+c^2)/b^4)*b^2-a*b*c+c^2)/(2*b*c),
      z = c/b}, {-a^4+4*a^2*b-4*a*c-2*b^2+P}],
    [{x = -(sqrt(c^2*(a^2*b^2-2*a*b*c-4*b^3+c^2)/b^4)*b^2-a*b*c+c^2)/(2*b*c),
      y = (sqrt(c^2*(a^2*b^2-2*a*b*c-4*b^3+c^2)/b^4)*b^2+a*b*c-c^2)/(2*b*c),
      z = c/b}, {-a^4+4*a^2*b-4*a*c-2*b^2+P}]

The expression for P is fine, but how are x and y square roots and z=c/b??

2.

eliminate({y*z, x+y-z}, z);
                       [{z = 0}, {x + y}]

Is this supposed to happen? I was expecting y*(x+y):

Groebner:-Basis({y*z, x+y-z}, lexdeg([z], [x, y]));
                     [x*y + y^2, z - x - y]

The documentation for the option AllSolutions for int says that the results are always valid for all real parameter values (in the endpoints). That seems like a pretty major claim. Each of these three is already wrong for a=-1/2, b=1/2:

int(1/ln(t), t = a .. b, AllSolutions);
    piecewise(ln(a) < ln(b), piecewise(And(1 < b, a < 1), undefined, piecewise(a = 1, infinity,
    Ei(1, -ln(a)))+piecewise(b = 1, -infinity, -Ei(1, -ln(b)))), ln(b) = ln(a), 0, ln(b) < ln(a),
    -piecewise(And(1 < a, b < 1), undefined, piecewise(b = 1, infinity, Ei(1, -ln(b)))+
    piecewise(a = 1, -infinity, -Ei(1, -ln(a)))))

int(sqrt(t^2-1+I*t), t = a .. b, AllSolutions);
    piecewise(a < b, (1/2)*sqrt(b^2-1+I*b)*b+I*sqrt(b^2-1+I*b)*(1/4)-3*ln(-2*signum(0, -b, 1)^2*
    b^2+2*sqrt(b^4-b^2+1)*signum(0, -b, 1)^2+4*b*sqrt(2*sqrt(b^4-b^2+1)+2*b^2-2)+2*
    signum(0, -b, 1)^2-2*signum(0, -b, 1)*sqrt(2*sqrt(b^4-b^2+1)-2*b^2+2)+6*b^2+2*
    sqrt(b^4-b^2+1)-1)*(1/16)-3*ln((-I*(signum(0, -b, 1)*sqrt(2*sqrt(b^4-b^2+1)-2*b^2+2)-1+I*
    sqrt(2*sqrt(b^4-b^2+1)+2*b^2-2)+(2*I)*b))*(1/sqrt(-2*signum(0, -b, 1)^2*b^2+2*sqrt(b^4-b^2+1)*
    signum(0, -b, 1)^2+4*b*sqrt(2*sqrt(b^4-b^2+1)+2*b^2-2)+2*signum(0, -b, 1)^2-2*signum(0, -b, 1)*
    sqrt(2*sqrt(b^4-b^2+1)-2*b^2+2)+6*b^2+2*sqrt(b^4-b^2+1)-1)))*(1/8)-(1/2)*sqrt(a^2-1+I*a)*a-I*
    sqrt(a^2-1+I*a)*(1/4)+3*ln(-2*signum(0, -a, -1)^2*a^2+2*sqrt(a^4-a^2+1)*signum(0, -a, -1)^2+
    4*a*sqrt(2*sqrt(a^4-a^2+1)+2*a^2-2)+2*signum(0, -a, -1)^2-2*signum(0, -a, -1)*sqrt(2*
    sqrt(a^4-a^2+1)-2*a^2+2)+6*a^2+2*sqrt(a^4-a^2+1)-1)*(1/16)+3*ln((-I*(signum(0, -a, -1)*sqrt(2*
    sqrt(a^4-a^2+1)-2*a^2+2)+I*sqrt(2*sqrt(a^4-a^2+1)+2*a^2-2)-1+(2*I)*a))*(1/sqrt(-2*
    signum(0, -a, -1)^2*a^2+2*sqrt(a^4-a^2+1)*signum(0, -a, -1)^2+4*a*sqrt(2*sqrt(a^4-a^2+1)+2*
    a^2-2)+2*signum(0, -a, -1)^2-2*signum(0, -a, -1)*sqrt(2*sqrt(a^4-a^2+1)-2*a^2+2)+6*a^2+2*
    sqrt(a^4-a^2+1)-1)))*(1/8), b = a, 0, b < a, -(1/2)*sqrt(a^2-1+I*a)*a-I*sqrt(a^2-1+I*a)*(1/4)+
    3*ln(-2*signum(0, -a, 1)^2*a^2+2*signum(0, -a, 1)^2*sqrt(a^4-a^2+1)+4*a*sqrt(2*sqrt(a^4-a^2+1)+
    2*a^2-2)+2*signum(0, -a, 1)^2-2*signum(0, -a, 1)*sqrt(2*sqrt(a^4-a^2+1)-2*a^2+2)+6*a^2+
    2*sqrt(a^4-a^2+1)-1)*(1/16)+3*ln((-I*(signum(0, -a, 1)*sqrt(2*sqrt(a^4-a^2+1)-2*a^2+2)+
    I*sqrt(2*sqrt(a^4-a^2+1)+2*a^2-2)-1+(2*I)*a))*(1/sqrt(-2*signum(0, -a, 1)^2*a^2+
    2*signum(0, -a, 1)^2*sqrt(a^4-a^2+1)+4*a*sqrt(2*sqrt(a^4-a^2+1)+2*a^2-2)+2*signum(0, -a, 1)^2-
    2*signum(0, -a, 1)*sqrt(2*sqrt(a^4-a^2+1)-2*a^2+2)+6*a^2+2*sqrt(a^4-a^2+1)-1)))*(1/8)+(1/2)*
    sqrt(b^2-1+I*b)*b+I*sqrt(b^2-1+I*b)*(1/4)-3*ln(-2*signum(0, -b, -1)^2*b^2+2*sqrt(b^4-b^2+1)*
    signum(0, -b, -1)^2+4*b*sqrt(2*sqrt(b^4-b^2+1)+2*b^2-2)+2*signum(0, -b, -1)^2-
    2*signum(0, -b, -1)*sqrt(2*sqrt(b^4-b^2+1)-2*b^2+2)+6*b^2+2*sqrt(b^4-b^2+1)-1)*(1/16)-
    3*ln(-(I*signum(0, -b, -1)*sqrt(2*sqrt(b^4-b^2+1)-2*b^2+2)-I-sqrt(2*sqrt(b^4-b^2+1)+2*b^2-2)-
    2*b)/sqrt(-2*signum(0, -b, -1)^2*b^2+2*sqrt(b^4-b^2+1)*signum(0, -b, -1)^2+4*b*sqrt(2*
    sqrt(b^4-b^2+1)+2*b^2-2)+2*signum(0, -b, -1)^2-2*signum(0, -b, -1)*sqrt(2*sqrt(b^4-b^2+1)-
    2*b^2+2)+6*b^2+2*sqrt(b^4-b^2+1)-1))*(1/8))

int(arctan(t+2*I), t = a .. b, AllSolutions);
   piecewise(a < b, piecewise(a < 0, I*arctan(4*a/(a^2-3))*(1/2)+(1/4)*ln(a^2+1)+(1/4)*ln(a^2+9)-
   (2*I)*arctan(2*I+a)-arctan(2*I+a)*a+I*Pi*(1/2), a = 0, -I*Pi+3*ln(3)*(1/2), 0 < a, I*arctan(4*a/
   (a^2-3))*(1/2)+(1/4)*ln(a^2+1)+(1/4)*ln(a^2+9)-(2*I)*arctan(2*I+a)-arctan(2*I+a)*a-I*Pi*(1/2))+
   piecewise(b < 0, -I*arctan(4*b/(b^2-3))*(1/2)-(1/4)*ln(b^2+1)-(1/4)*ln(b^2+9)+(2*I)*
   arctan(2*I+b)+arctan(2*I+b)*b-I*Pi*(1/2), b = 0, -I*Pi-3*ln(3)*(1/2), 0 < b, -I*arctan(4*b/
   (b^2-3))*(1/2)-(1/4)*ln(b^2+1)-(1/4)*ln(b^2+9)+(2*I)*arctan(2*I+b)+arctan(2*I+b)*b+I*Pi*(1/2))+
   piecewise(And(0 < b, a < 0), -(2*I)*Pi, 0), b = a, 0, b < a, piecewise(b < 0, -I*arctan(4*b/
   (b^2-3))*(1/2)-(1/4)*ln(b^2+1)-(1/4)*ln(b^2+9)+(2*I)*arctan(2*I+b)+arctan(2*I+b)*b-I*Pi*(1/2),
   b = 0, I*Pi-3*ln(3)*(1/2), 0 < b, -I*arctan(4*b/(b^2-3))*(1/2)-(1/4)*ln(b^2+1)-(1/4)*ln(b^2+9)+
   (2*I)*arctan(2*I+b)+arctan(2*I+b)*b+I*Pi*(1/2))+piecewise(a < 0, I*arctan(4*a/(a^2-3))*(1/2)+
   (1/4)*ln(a^2+1)+(1/4)*ln(a^2+9)-(2*I)*arctan(2*I+a)-arctan(2*I+a)*a+I*Pi*(1/2), a = 0,
   I*Pi+3*ln(3)*(1/2), 0 < a, I*arctan(4*a/(a^2-3))*(1/2)+(1/4)*ln(a^2+1)+(1/4)*ln(a^2+9)-(2*I)*
   arctan(2*I+a)-arctan(2*I+a)*a-I*Pi*(1/2))-piecewise(And(0 < a, b < 0), -(2*I)*Pi, 0))

The first one probably has the correct answer inside, but it has conditions like ln(a)<ln(b), so that case never gets selected when the values are complex.

f := (z, t) -> ln(t)^2/((t^2+1)*(t-z));

int(f(z, t), t = 0 .. infinity) assuming Im(z) > 0;
       int(ln(t)^2/((t^2+1)*(t-z)), t = 0 .. infinity)

int(f(a + I*b, t), t = 0 .. infinity) assuming a::real, b > 0; # 0*infinity
       -sqrt(a^2+b^2-2*b+1)*signum(I*arctan(b, a)-I*arctan(-b, -a)-I*Pi)*
       infinity/((I*b-I+a)*(I*b+I+a))

int(f(z, t), t = 0 .. infinity) assuming Re(z) > 0, Im(z) > 0;
       int(ln(t)^2/((t^2+1)*(t-z)), t = 0 .. infinity)

int(f(a + I*b, t), t = 0 .. infinity) assuming a > 0, b > 0;
      -((3*I)*Pi^3*b+3*Pi^3*a-(16*I)*Pi^2*arctan(b/a)-(6*I)*Pi*ln(a^2+b^2)^2+(24*I)*
      Pi*arctan(b/a)^2+(6*I)*ln(a^2+b^2)^2*arctan(b/a)-(8*I)*arctan(b/a)^3-8*Pi^2*
      ln(a^2+b^2)+24*Pi*ln(a^2+b^2)*arctan(b/a)+ln(a^2+b^2)^3-12*ln(a^2+b^2)*
      arctan(b/a)^2)/(24*(-b^2+(2*I)*a*b+a^2+1))

So it looks like the first three can be made to work as well (and the result in terms of z will be much neater).

a::real and b::real;
Error, type `real` does not exist

`and`(a::real, b::real);
                       a::real and b::real

Since a::real by itself is fine, why does the conjunction give an error?

These two are evaluated differently as well:

Im(a) > 0 and a <> 0;
                           0 < Im(a)
`and`(Im(a) > 0, a <> 0);
                      0 < Im(a) and a <> 0

The consequence is that these two will work differently:

is(a <> 0) assuming Im(a) > 0 and a <> 0;
                             FAIL

is(a <> 0) assuming `and`(Im(a) > 0, a <> 0);
                             true

is(a <> 0) assuming Im(a) > 0; # sadly, just Im(a) > 0 is not enough
                             FAIL

It looks like (a and b) and `and`(a, b) just do completely different things:

x := proc() local r; r := rand(); print(r); r end proc;

a > x() and a > x() and a = a;
                          395718860534
                        395718860534 < a

`and`(a > x(), a > x(), a = a);
                          193139816415
                          22424170465
         193139816415 < a and 22424170465 < a and a = a

That is, (a and b) first simplifed the expression and then evaluated a>x() once, but `and`(a, b) evaluated the arguments without doing any simplifications.

Also, should this work (it works with `real`, which supposedly doesn't exist):

Re(a+b) assuming a::realcons, b::realcons;
                           Re(a + b)