common_proof_rules.h

Go to the documentation of this file.
00001 /*****************************************************************************/
00002 /*!
00003  * \file common_proof_rules.h
00004  * 
00005  * Author: Sergey Berezin
00006  * 
00007  * Created: Dec 11 18:15:37 GMT 2002
00008  *
00009  * <hr>
00010  *
00011  * License to use, copy, modify, sell and/or distribute this software
00012  * and its documentation for any purpose is hereby granted without
00013  * royalty, subject to the terms and conditions defined in the \ref
00014  * LICENSE file provided with this distribution.
00015  * 
00016  * <hr>
00017  * 
00018  */
00019 /*****************************************************************************/
00020 // CLASS: CommonProofRules
00021 //
00022 // AUTHOR: Sergey Berezin, 12/09/2002
00023 //
00024 // Description: Commonly used proof rules (reflexivity, symmetry,
00025 // transitivity, substitutivity, etc.).
00026 //
00027 // Normally, proof rule interfaces belong to their decision
00028 // procedures.  However, in the case of equational logic, the rules
00029 // are so useful, that even some basic classes like Transformer use
00030 // these rules under the hood.  Therefore, it is made public, and its
00031 // implementation is provided by the 'theorem' module.
00032 ///////////////////////////////////////////////////////////////////////////////
00033 
00034 #ifndef _cvc3__common_proof_rules_h_
00035 #define _cvc3__common_proof_rules_h_
00036 
00037 #include <vector>
00038 
00039 namespace CVC3 {
00040 
00041   class Theorem;
00042   class Theorem3;
00043   class Expr;
00044   class Op;
00045 
00046   class CommonProofRules {
00047   public:
00048     //! Destructor
00049     virtual ~CommonProofRules() { }
00050 
00051     ////////////////////////////////////////////////////////////////////////
00052     // TCC rules (3-valued logic)
00053     ////////////////////////////////////////////////////////////////////////
00054 
00055     //  G1 |- phi   G2 |- D_phi
00056     // -------------------------
00057     //       G1,G2 |-_3 phi
00058     /*!
00059      * @brief Convert 2-valued formula to 3-valued by discharging its
00060      *  TCC (\f$D_\phi\f$):
00061      *  \f[\frac{\Gamma_1\vdash_2 \phi\quad \Gamma_2\vdash_2 D_{\phi}}
00062      *          {\Gamma_1,\,\Gamma_2\vdash_3\phi}\f]
00063      */
00064     virtual Theorem3 queryTCC(const Theorem& phi, const Theorem& D_phi) = 0;
00065 
00066     //  G0,a1,...,an |-_3 phi  G1 |- D_a1 ... Gn |- D_an
00067     // -------------------------------------------------
00068     //    G0,G1,...,Gn |-_3 (a1 & ... & an) -> phi
00069     /*!
00070      * @brief 3-valued implication introduction rule:
00071      * \f[\frac{\Gamma_0,\,\alpha_1\,\ldots,\,\alpha_n\vdash_3\phi\quad
00072      *          (\Gamma_i\vdash D_{\alpha_i})_{i\in[1..n]}}
00073      *         {\Gamma_0,\,\Gamma_1, \ldots, \Gamma_n\vdash_3
00074      *              (\bigwedge_{i=1}^n\alpha_i)\to\phi}\f]
00075      *
00076      * \param phi is the formula \f$\phi\f$
00077      * \param assump is the vector of assumptions \f$\alpha_1\ldots\alpha_n\f$
00078      * \param tccs is the vector of TCCs for assumptions
00079      *   \f$D_{\alpha_1}\ldots D_{\alpha_n}\f$
00080      */
00081     virtual Theorem3 implIntro3(const Theorem3& phi,
00082         const std::vector<Expr>& assump,
00083         const std::vector<Theorem>& tccs) = 0;
00084 
00085     ////////////////////////////////////////////////////////////////////////
00086     // Common rules
00087     ////////////////////////////////////////////////////////////////////////
00088 
00089     // ==> u:a |- a
00090     //! \f[\frac{}{a\vdash a}\f]
00091     virtual Theorem assumpRule(const Expr& a, int scope = -1) = 0;
00092 
00093     //  ==> a == a   or   ==> a IFF a
00094     //! \f[\frac{}{a = a}\quad or \quad\frac{}{a \Leftrightarrow a}\f]
00095     virtual Theorem reflexivityRule(const Expr& a) = 0;
00096 
00097     //! ==> (a == a) IFF TRUE
00098     virtual Theorem rewriteReflexivity(const Expr& a_eq_a) = 0;
00099 
00100     //  a1 == a2 ==> a2 == a1 (same for IFF)
00101     //! \f[\frac{a_1=a_2}{a_2=a_1}\f] (same for IFF)
00102     virtual Theorem symmetryRule(const Theorem& a1_eq_a2) = 0;
00103 
00104     // ==> (a1 == a2) IFF (a2 == a1)
00105     //! \f[\frac{}{(a_1=a_2)\Leftrightarrow (a_2=a_1)}\f]
00106     virtual Theorem rewriteUsingSymmetry(const Expr& a1_eq_a2) = 0;
00107 
00108     // (a1 == a2) & (a2 == a3) ==> (a1 == a3) [same for IFF]
00109     //! \f[\frac{a_1=a_2\quad a_2=a_3}{a_1=a_3}\f] (same for IFF)
00110     virtual Theorem transitivityRule(const Theorem& a1_eq_a2,
00111                                      const Theorem& a2_eq_a3) = 0;
00112 
00113     //! Optimized case for expr with one child
00114     virtual Theorem substitutivityRule(const Expr& e, const Theorem& thm) = 0;
00115 
00116     //! Optimized case for expr with two children
00117     virtual Theorem substitutivityRule(const Expr& e, const Theorem& thm1,
00118                                        const Theorem& thm2) = 0;
00119 
00120     // (c_1 == d_1) & ... & (c_n == d_n)
00121     //   ==> op(c_1,...,c_n) == op(d_1,...,d_n)
00122     /*! @brief 
00123       \f[\frac{(c_1=d_1)\wedge\ldots\wedge(c_n=d_n)}
00124               {op(c_1,\ldots,c_n)=op(d_1,\ldots,d_n)}\f]
00125     */
00126     virtual Theorem substitutivityRule(const Op& op,
00127                                        const std::vector<Theorem>& thms) = 0;
00128 
00129     // (c_1 == d_1) & ... & (c_n == d_n)
00130     //   ==> op(c_1,...,c_n) == op(d_1,...,d_n)
00131     /*! @brief 
00132       \f[\frac{(c_1=d_1)\wedge\ldots\wedge(c_n=d_n)}
00133               {op(c_1,\ldots,c_n)=op(d_1,\ldots,d_n)}\f]
00134       except that only those arguments are given that \f$c_i\not=d_i\f$.
00135       \param e is the original expression \f$op(c_1,\ldots,c_n)\f$.
00136       \param changed is the vector of indices of changed kids
00137       \param thms are the theorems \f$c_i=d_i\f$ for the changed kids.
00138     */
00139     virtual Theorem substitutivityRule(const Expr& e,
00140                                        const std::vector<unsigned>& changed,
00141                                        const std::vector<Theorem>& thms) = 0;
00142     virtual Theorem substitutivityRule(const Expr& e, const int changed, const Theorem& thm) = 0;
00143 
00144     // |- e,  |- !e ==> |- FALSE
00145     /*! @brief
00146       \f[\frac{\Gamma_1\vdash e\quad\Gamma_2\vdash \neg e}
00147               {\Gamma_1\cup\Gamma_2\vdash \mathrm{FALSE}}
00148       \f]
00149      */
00150     virtual Theorem contradictionRule(const Theorem& e,
00151               const Theorem& not_e) = 0;
00152 
00153     // |- e OR !e
00154     virtual Theorem excludedMiddle(const Expr& e) = 0;
00155 
00156     // e ==> e IFF TRUE
00157     //! \f[\frac{\Gamma\vdash e}{\Gamma\vdash e\Leftrightarrow\mathrm{TRUE}}\f]
00158     virtual Theorem iffTrue(const Theorem& e) = 0;
00159 
00160     // e ==> !e IFF FALSE
00161     //! \f[\frac{\Gamma\vdash e}{\Gamma\vdash\neg e\Leftrightarrow\mathrm{FALSE}}\f]
00162     virtual Theorem iffNotFalse(const Theorem& e) = 0;
00163 
00164     // e IFF TRUE ==> e
00165     //! \f[\frac{\Gamma\vdash e\Leftrightarrow\mathrm{TRUE}}{\Gamma\vdash e}\f]
00166     virtual Theorem iffTrueElim(const Theorem& e) = 0;
00167 
00168     // e IFF FALSE ==> !e
00169     //! \f[\frac{\Gamma\vdash e\Leftrightarrow\mathrm{FALSE}}{\Gamma\vdash\neg e}\f]
00170     virtual Theorem iffFalseElim(const Theorem& e) = 0;
00171 
00172     //! e1 <=> e2  ==>  ~e1 <=> ~e2
00173     /*!  \f[\frac{\Gamma\vdash e_1\Leftrightarrow e_2}
00174      *           {\Gamma\vdash\sim e_1\Leftrightarrow\sim e_2}\f]
00175      * Where ~e is the <em>inverse</em> of e (that is, ~(!e') = e').
00176      */
00177     virtual Theorem iffContrapositive(const Theorem& thm) = 0;
00178 
00179     // !!e ==> e
00180     //! \f[\frac{\Gamma\vdash\neg\neg e}{\Gamma\vdash e}\f]
00181     virtual Theorem notNotElim(const Theorem& not_not_e) = 0;
00182 
00183     // e1 AND (e1 IFF e2) ==> e2
00184     /*! @brief
00185       \f[\frac{\Gamma_1\vdash e_1\quad \Gamma_2\vdash(e_1\Leftrightarrow e_2)}
00186               {\Gamma_1\cup\Gamma_2\vdash e_2}
00187       \f]
00188     */
00189     virtual Theorem iffMP(const Theorem& e1, const Theorem& e1_iff_e2) = 0;
00190 
00191     // e1 AND (e1 IMPLIES e2) ==> e2
00192     /*! @brief
00193       \f[\frac{\Gamma_1\vdash e_1\quad \Gamma_2\vdash(e_1\Rightarrow e_2)}
00194               {\Gamma_1\cup\Gamma_2\vdash e_2}
00195       \f]
00196     */
00197     virtual Theorem implMP(const Theorem& e1, const Theorem& e1_impl_e2) = 0;
00198 
00199     // AND(e_1,...e_n) ==> e_i
00200     //! \f[\frac{\vdash e_1\wedge\cdots\wedge e_n}{\vdash e_i}\f]
00201     virtual Theorem andElim(const Theorem& e, int i) = 0;
00202 
00203     // e1, e2 ==> AND(e1, e2)
00204     /*! @brief
00205       \f[\frac{\Gamma_1\vdash e_1\quad \Gamma_2\vdash e_2}
00206               {\Gamma_1\cup\Gamma_2\vdash e_1\wedge e_2}
00207       \f]
00208     */
00209     virtual Theorem andIntro(const Theorem& e1, const Theorem& e2) = 0;
00210 
00211     // e1, ..., en ==> AND(e1, ..., en)
00212     /*! @brief
00213       \f[\frac{\Gamma_1\vdash e_1\quad \cdots \quad\Gamma_n\vdash e_n}
00214               {\bigcup_{i=1}^n\Gamma_i\vdash \bigwedge_{i=1}^n e_i}
00215       \f]
00216     */
00217     virtual Theorem andIntro(const std::vector<Theorem>& es) = 0;
00218 
00219     //  G,a1,...,an |- phi
00220     // -------------------------------------------------
00221     //    G |- (a1 & ... & an) -> phi
00222     /*!
00223      * @brief Implication introduction rule:
00224      * \f[\frac{\Gamma,\,\alpha_1\,\ldots,\,\alpha_n\vdash\phi}
00225      *         {\Gamma\vdash(\bigwedge_{i=1}^n\alpha_i)\to\phi}\f]
00226      *
00227      * \param phi is the formula \f$\phi\f$
00228      * \param assump is the vector of assumptions \f$\alpha_1\ldots\alpha_n\f$
00229      */
00230     virtual Theorem implIntro(const Theorem& phi,
00231             const std::vector<Expr>& assump) = 0;
00232 
00233     //! e1 => e2  ==>  ~e2 => ~e1
00234     /*!  \f[\frac{\Gamma\vdash e_1\Rightarrow e_2}
00235      *           {\Gamma\vdash\sim e_2\Rightarrow\sim e_1}\f]
00236      * Where ~e is the <em>inverse</em> of e (that is, ~(!e') = e').
00237      */
00238     virtual Theorem implContrapositive(const Theorem& thm) = 0;
00239 
00240     // NOT e ==> e IFF FALSE
00241     //! \f[\frac{\vdash\neg e}{\vdash e\Leftrightarrow\mathrm{FALSE}}\f]
00242     virtual Theorem notToIff(const Theorem& not_e) = 0;
00243 
00244     // e1 XOR e2 ==> e1 IFF (NOT e2)
00245     //! \f[\frac{\vdash e_1 XOR e_2}{\vdash e_1\Leftrightarrow(\neg e_2)}\f]
00246     virtual Theorem xorToIff(const Expr& e) = 0;
00247 
00248     //! ==> (e1 <=> e2) <=> [simplified expr]
00249     /*! Rewrite formulas like FALSE/TRUE <=> e,  e <=> NOT e, etc. */
00250     virtual Theorem rewriteIff(const Expr& e) = 0;
00251 
00252     // AND and OR rewrites check for TRUE and FALSE arguments and
00253     // remove them or collapse the entire expression to TRUE and FALSE
00254     // appropriately
00255 
00256     //! ==> AND(e1,e2) IFF [simplified expr]
00257     virtual Theorem rewriteAnd(const Expr& e) = 0;
00258 
00259     //! ==> OR(e1,...,en) IFF [simplified expr]
00260     virtual Theorem rewriteOr(const Expr& e) = 0;
00261 
00262     //! ==> NOT TRUE IFF FALSE
00263     virtual Theorem rewriteNotTrue(const Expr& e) = 0;
00264 
00265     //! ==> NOT FALSE IFF TRUE
00266     virtual Theorem rewriteNotFalse(const Expr& e) = 0;
00267 
00268     //! ==> NOT NOT e IFF e, takes !!e
00269     virtual Theorem rewriteNotNot(const Expr& e) = 0;
00270 
00271     //! ==> NOT FORALL (vars): e  IFF EXISTS (vars) NOT e
00272     virtual Theorem rewriteNotForall(const Expr& forallExpr) = 0;
00273 
00274     //! ==> NOT EXISTS (vars): e  IFF FORALL (vars) NOT e
00275     virtual Theorem rewriteNotExists(const Expr& existsExpr) = 0;
00276 
00277     //From expr EXISTS(x1: t1, ..., xn: tn) phi(x1,...,cn)
00278     //we create phi(c1,...,cn) where ci is a skolem constant
00279     //defined by the original expression and the index i.
00280     virtual Expr skolemize(const Expr& e) = 0;
00281 
00282     /*! skolem rewrite rule: Introduces axiom |- Exists(x) phi(x) <=> phi(c)
00283      * where c is a constant defined by the expression Exists(x) phi(x)
00284      */
00285     virtual Theorem skolemizeRewrite(const Expr& e) = 0;
00286 
00287     //! Special version of skolemizeRewrite for "EXISTS x. t = x"
00288     virtual Theorem skolemizeRewriteVar(const Expr& e) = 0;
00289 
00290     //! |- EXISTS x. e = x
00291     virtual Theorem varIntroRule(const Expr& e) = 0;
00292 
00293     /*! @brief If thm is (EXISTS x: phi(x)), create the Skolemized version
00294       and add it to the database.  Otherwise returns just thm. */
00295     /*!
00296      * \param thm is the Theorem(EXISTS x: phi(x))
00297      */
00298     virtual Theorem skolemize(const Theorem& thm) = 0;
00299 
00300     //! Retrun a theorem "|- e = v" for a new Skolem constant v
00301     /*!
00302      * This is equivalent to skolemize(d_core->varIntroRule(e)), only more
00303      * efficient.
00304      */
00305     virtual Theorem varIntroSkolem(const Expr& e) = 0;
00306 
00307     // Derived rules
00308 
00309     //! ==> TRUE
00310     virtual Theorem trueTheorem() = 0;
00311 
00312     //! AND(e1,e2) ==> [simplified expr]
00313     virtual Theorem rewriteAnd(const Theorem& e) = 0;
00314 
00315     //! OR(e1,...,en) ==> [simplified expr]
00316     virtual Theorem rewriteOr(const Theorem& e) = 0;
00317 
00318     // TODO: do we really need this?
00319     virtual std::vector<Theorem>& getSkolemAxioms() = 0;
00320 
00321     //TODO: do we need this?
00322     virtual void clearSkolemAxioms() = 0;
00323 
00324     virtual Theorem ackermann(const Expr& e1, const Expr& e2) = 0;
00325 
00326   }; // end of class CommonProofRules
00327 
00328 } // end of namespace CVC3
00329 
00330 #endif

Generated on Tue Jul 3 14:33:35 2007 for CVC3 by  doxygen 1.5.1