CVCL::CommonProofRules Member List

This is the complete list of members for CVCL::CommonProofRules, including all inherited members.

andElim(const Theorem &e, int i)=0CVCL::CommonProofRules [pure virtual]
andIntro(const Theorem &e1, const Theorem &e2)=0CVCL::CommonProofRules [pure virtual]
andIntro(const std::vector< Theorem > &es)=0CVCL::CommonProofRules [pure virtual]
assumpRule(const Expr &a, int scope=-1)=0CVCL::CommonProofRules [pure virtual]
clearSkolemAxioms()=0CVCL::CommonProofRules [pure virtual]
contradictionRule(const Theorem &e, const Theorem &not_e)=0CVCL::CommonProofRules [pure virtual]
getSkolemAxioms()=0CVCL::CommonProofRules [pure virtual]
iffContrapositive(const Theorem &thm)=0CVCL::CommonProofRules [pure virtual]
iffFalseElim(const Theorem &e)=0CVCL::CommonProofRules [pure virtual]
iffMP(const Theorem &e1, const Theorem &e1_iff_e2)=0CVCL::CommonProofRules [pure virtual]
iffNotFalse(const Theorem &e)=0CVCL::CommonProofRules [pure virtual]
iffTrue(const Theorem &e)=0CVCL::CommonProofRules [pure virtual]
iffTrueElim(const Theorem &e)=0CVCL::CommonProofRules [pure virtual]
implContrapositive(const Theorem &thm)=0CVCL::CommonProofRules [pure virtual]
implIntro(const Theorem &phi, const std::vector< Expr > &assump)=0CVCL::CommonProofRules [pure virtual]
implMP(const Theorem &e1, const Theorem &e1_impl_e2)=0CVCL::CommonProofRules [pure virtual]
notNotElim(const Theorem &not_not_e)=0CVCL::CommonProofRules [pure virtual]
notToIff(const Theorem &not_e)=0CVCL::CommonProofRules [pure virtual]
reflexivityRule(const Expr &a)=0CVCL::CommonProofRules [pure virtual]
rewriteAnd(const Expr &e)=0CVCL::CommonProofRules [pure virtual]
rewriteAnd(const Theorem &e)=0CVCL::CommonProofRules [pure virtual]
rewriteIff(const Expr &e)=0CVCL::CommonProofRules [pure virtual]
rewriteNotExists(const Expr &existsExpr)=0CVCL::CommonProofRules [pure virtual]
rewriteNotFalse(const Expr &e)=0CVCL::CommonProofRules [pure virtual]
rewriteNotForall(const Expr &forallExpr)=0CVCL::CommonProofRules [pure virtual]
rewriteNotNot(const Expr &e)=0CVCL::CommonProofRules [pure virtual]
rewriteNotTrue(const Expr &e)=0CVCL::CommonProofRules [pure virtual]
rewriteOr(const Expr &e)=0CVCL::CommonProofRules [pure virtual]
rewriteOr(const Theorem &e)=0CVCL::CommonProofRules [pure virtual]
rewriteReflexivity(const Expr &a_eq_a)=0CVCL::CommonProofRules [pure virtual]
rewriteUsingSymmetry(const Expr &a1_eq_a2)=0CVCL::CommonProofRules [pure virtual]
skolemize(const Expr &e)=0CVCL::CommonProofRules [pure virtual]
skolemize(const Theorem &thm)=0CVCL::CommonProofRules [pure virtual]
skolemizeRewrite(const Expr &e)=0CVCL::CommonProofRules [pure virtual]
skolemizeRewriteVar(const Expr &e)=0CVCL::CommonProofRules [pure virtual]
substitutivityRule(const Op &op, const std::vector< Theorem > &thms)=0CVCL::CommonProofRules [pure virtual]
substitutivityRule(const Expr &e, const std::vector< unsigned > &changed, const std::vector< Theorem > &thms)=0CVCL::CommonProofRules [pure virtual]
symmetryRule(const Theorem &a1_eq_a2)=0CVCL::CommonProofRules [pure virtual]
transitivityRule(const Theorem &a1_eq_a2, const Theorem &a2_eq_a3)=0CVCL::CommonProofRules [pure virtual]
trueTheorem()=0CVCL::CommonProofRules [pure virtual]
varIntroRule(const Expr &e)=0CVCL::CommonProofRules [pure virtual]
varIntroSkolem(const Expr &e)=0CVCL::CommonProofRules [pure virtual]
~CommonProofRules()CVCL::CommonProofRules [inline, virtual]


Generated on Thu Apr 13 16:57:42 2006 for CVC Lite by  doxygen 1.4.4