As defined for use NAT-DED: is a primitive tactic.

Applies PUSHNEG if a support line is a negated non-literal formula.

If any support line is a negated formula, calls the appropriate tactic

for pushing the negation in.

As defined for use ETREE-NAT:

(IFTHEN (NEG-SLINE-P-TAC)

(ORELSE NEG-NEG-SLINE-TAC NEG-OR-SLINE-TAC NEG-IMP-SLINE-TAC

NEG-SEL-SLINE-TAC NEG-EXP-SLINE-TAC NEG-REW-SLINE-TAC))

If any support line is a negated formula, calls the appropriate tactic

for pushing the negation in.

© 1988-99, Carnegie Mellon University.