This chooses one of the two ways of constructing an etree

from an equivalence A EQUIV B:

1 chooses the option with the fewest vertical paths

(positive: A AND B OR ~A AND ~B

negative: A IMPLIES B AND B IMPLIES A)

2 chooses the option with the fewest horizontal paths

(negative: A AND B OR ~A AND ~B

positive: A IMPLIES B AND B IMPLIES A)

3 behaves as for 2 except for the first equivalence it finds,

when it behaves as for 1. (This means that a gwff which is a

quantified equivalence will produce an etree which can be split.)

4 always chooses A IMPLIES B AND B IMPLIES A

5 always chooses A AND B OR ~A AND ~B

Any other setting will behave like 1.

This does not work with MIN-QUANTIFIER-SCOPE T; in that case,

etrees will be constructed as in case 1, regardless of the setting

of this flag.

REWRITE-EQUIVS takes values of type POSINTEGER.

It belongs to subjects MS98-1 MS93-1 MS92-9 MS91-7 MS91-6 MS90-9 MS90-3 MS89 MS88 IMPORTANT MATING-SEARCH .

Its default value is 1

Its current value is 1.

© 1988-99, Carnegie Mellon University.