REWRITE-EQUIVS : FLAGREWRITE-EQUIVS is a flag or parameter.
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.
TPS documentation homepage