PP* : UNIFOPPP* is an unification command.
Displays the disagreement pairs at the current-topnode, including the order of
each pair and other information. See also PP. The other information displayed
includes (for each wff, each disagreement pair and the whole set of
1) the order (e.g. "x(i)" is first order, and so on).
2) whether it is monadic (all function constants are unary).
3) whether it is linear (all free vars occur once only).
4) whether it is a matching problem (one side of a dpair has no free vars).
5) whether it is a relaxed pattern (all free vars have only bound vars as
6) whether it is a pattern (all free vars have distinct bound vars as
7) whether a disagreement pair is variable-disjoint (the free vars on the
left are disjoint from those on the right).
8) whether the set of disagreement pairs can be partitioned into sets in
which each free var in the whole problem occurs in at most one set.
9) whether there are any free vars that occur only once, or not at all, in
the whole problem.
These conditions all appear in the literature on higher-order unification;
see, for example, Prehofer's paper in CADE '94.
More information about the current node is given by the command P.
PP* is a printing command.
TPS documentation homepage