TACTIC-EXP : ARGTYPE

TACTIC-EXP is an argument type.
Either the name of a tactic or a compound tactic expression.
Currently defined tactics are:
AUTO-TAC BOOK-TAC COMPLETE-TRANSFORM*-TAC COMPLETE-TRANSFORM-TAC DIY-TAC ELIM-DEFNS-TAC GO2-TAC MIN-PROP MONSTRO-TAC PFENNING*-TAC PFENNING-TAC PLINE-TAC PROP-ELIM-RULES-TAC PROP-INTRO-RULES-TAC REWRITE-PLINE-P-TAC REWRITE-PLINE-TAC REWRITE-SLINE-TAC SLINE-TAC SUB=-TAC ABSURD-TAC BACKCHAIN-LEMMA-TAC CASES-TAC CLASS-DISJ-TAC DEDUCT-TAC DISJ-EQUIV-TAC DISJ-IMP-TAC ECONJ*-TAC ECONJ-TAC ENEG-TAC EQUIV-DISJ-TAC EQUIV-IMPLICS-TAC ICONJ*-TAC ICONJ-TAC IDISJ-LEFT-TAC IDISJ-RIGHT-TAC IDISJ-TAC IMP-DISJ-TAC IMPLICS-EQUIV-TAC INDIRECT-DISJ-PLINE-TAC INDIRECT-EXISTS-PLINE-TAC INDIRECT-TAC INDIRECT2-TAC INEG-TAC MP-TAC NEG-AND-ELIM-TAC NEG-AND-PLAN-TAC NEG-AND-SLINE-TAC NEG-ATOM-ELIM-TAC NEG-EQUAL-ELIM-TAC NEG-EXISTS-ELIM-DUP-TAC NEG-EXISTS-ELIM-SIMPLE-TAC NEG-IMP-ELIM-TAC NEG-IMP-PLAN-TAC NEG-IMP-SLINE-TAC NEG-NEG-ELIM-TAC NEG-NEG-PLAN-TAC NEG-NEG-SLINE-TAC NEG-OR-ELIM-DUP-TAC NEG-OR-ELIM-SIMPLE-TAC NEG-OR-PLAN-TAC NEG-OR-SLINE-TAC NEG-UNIV-ELIM-TAC OR-LEMMA-LEFT-TAC OR-LEMMA-RIGHT-TAC OR-LEMMA-TAC PROP-PRIM PROPOSITIONAL PULLNEG-TAC PUSHNEG-TAC RULEP-TAC SAME-TAC SUBST=-BACKCHAIN-LEMMA-TAC TRUTH-TAC ML::TRUTHP-REWRITE-PLAN-TAC AB-PLAN-TAC AB-SLINE-TAC ABU-TAC EDEF-TAC EGEN-TAC EXISTS-LEMMA-TAC IDEF-TAC NEG-EXP-PLAN-TAC NEG-EXP-SLINE-TAC NEG-SEL-PLAN-TAC NEG-SEL-SLINE-TAC QUANTIFICATIONAL RULEC-TAC RULEQ-PLAN-TAC RULEQ-SLINE-TAC SYMSIMP-TAC UGEN-TAC UI-HERBRAND-TAC UI-TAC UNNEC-EXP-TAC EQUALITY-PLAN-TAC EQUALITY-SLINE-TAC EXT=-PLAN-TAC EXT=-SLINE-TAC LEIBNIZ=-PLAN-TAC LEIBNIZ=-SLINE-TAC NEG-EQUAL-SLINE-TAC REFL=-TAC SUBST=-TAC SUBST=L-TAC SUBST=R-TAC SYM=-TAC EQUIV-WFFS-PLAN-TAC EQUIV-WFFS-SLINE-TAC NEG-REW-PLAN-TAC NEG-REW-SLINE-TAC BETA-ETA-SEPARATE-TAC BETA-ETA-TOGETHER-TAC BETA-ONLY-TAC EQUIV-EQ-CONTR-TAC EQUIV-EQ-EXPD-TAC EXT=-TAC EXT=0-TAC LCONTR*-BETA-TAC LCONTR*-ETA-TAC LCONTR*-TAC LCONTR*-VARY-TAC LEXPD*-BETA-TAC LEXPD*-ETA-TAC LEXPD*-TAC LEXPD*-VARY-TAC FINISHED-P INESS-PLINE-TAC MAKE-NICE MAKE-ROOM NEG-PLINE-P-TAC NEG-SLINE-P-TAC RESTRICT-MATING-TAC REWRITE-SLINE-P-TAC SHOW-CURRENT-PLAN SHOW-PLANS UNIVERSAL-GOAL-P UNSPONSOR-TAC USE-RULEP-TAC USE-SYMSIMP-TAC .

TPS documentation homepage


© 1988-99, Carnegie Mellon University.

TPS homepage