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

disagreement pairs):

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

arguments).

6) whether it is a pattern (all free vars have distinct bound vars as

arguments).

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.

© 1988-99, Carnegie Mellon University.