PFENNING*-TAC : TACTIC

PFENNING*-TAC is a tactic.
As defined for use ETREE-NAT:
(ORELSE (CALL PRINT-ROUTINES) SAME-TAC ABSURD-TAC TRUTH-TAC REFL=-TAC
(MAKE-ROOM :USE NAT-DED) (THEN** ECONJ-TAC UNSPONSOR-TAC) DEDUCT-TAC
REWRITE-SLINE-TAC REWRITE-PLINE-TAC RULEC-TAC UGEN-TAC EGEN-TAC
(THEN** UI-TAC UNSPONSOR-TAC) (THEN** UNNEC-EXP-TAC UNSPONSOR-TAC)
(THEN** IDISJ-TAC UNSPONSOR-TAC) (THEN** ICONJ-TAC UNSPONSOR-TAC)
(THEN** CASES-TAC UNSPONSOR-TAC) INEG-TAC ENEG-TAC SUBST=L-TAC
SUBST=R-TAC MP-TAC (IFTHEN USE-SYMSIMP-TAC SYMSIMP-TAC CLASS-DISJ-TAC)
INESS-PLINE-TAC INDIRECT-TAC NEG-REW-SLINE-TAC)
Intended to be the same as the tactics advocated in Pfenning's thesis.

TPS documentation homepage


© 1988-99, Carnegie Mellon University.

TPS homepage