ENEG-TAC : TACTIC

ENEG-TAC is a tactic.
As defined for use NAT-DED: is a primitive tactic.
Applies ENEG if a support line is a negation and planned line is
FALSEHOOD.
As defined for use ETREE-NAT:
(ORELSE NEG-ATOM-ELIM-TAC NEG-NEG-ELIM-TAC NEG-AND-ELIM-TAC
NEG-IMP-ELIM-TAC NEG-UNIV-ELIM-TAC NEG-EXISTS-ELIM-SIMPLE-TAC
NEG-EXISTS-ELIM-DUP-TAC NEG-OR-ELIM-SIMPLE-TAC NEG-OR-ELIM-DUP-TAC
NEG-EQUAL-ELIM-TAC)

TPS documentation homepage


© 1988-99, Carnegie Mellon University.

TPS homepage