PULLNEG-TAC : TACTIC

PULLNEG-TAC is a tactic.
As defined for use NAT-DED: is a primitive tactic.
Applies PULLNEG if the planned line is a negated non-literal formula.
If planned line is a negated formula, calls the appropriate tactic
for pulling the negation out.
As defined for use ETREE-NAT:
(IFTHEN (NEG-PLINE-P-TAC)
(ORELSE NEG-NEG-PLAN-TAC NEG-OR-PLAN-TAC NEG-IMP-PLAN-TAC
NEG-SEL-PLAN-TAC NEG-EXP-PLAN-TAC NEG-REW-PLAN-TAC))
If planned line is a negated formula, calls the appropriate tactic
for pulling the negation out.

TPS documentation homepage


© 1988-99, Carnegie Mellon University.

TPS homepage