The tableau methods, in contrast, provide a technique for changing the boolean structure of a formula by constructing case distinctions. Compared to the standard simplifier they are much slower. For details on tableau simplification see section References . This is a list of atomic formulas considered as a disjunction. The result is a tableau wrt.
Tableau steps wrt.
Iterative automatic tableau method. The exact procedure depends on the switch rltabib . By default this switch is on. It controls the procedure rlitab . If rltabib is off, rlatab is iteratively applied to the argument formula as long as shorter results can be obtained.