PUSHNEG-TAC : TACTIC

PUSHNEG-TAC is a tactic.
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.

TPS documentation homepage


© 1988-99, Carnegie Mellon University.

TPS homepage