search_rules.h

Go to the documentation of this file.
00001 /*****************************************************************************/
00002 /*!
00003  * \file search_rules.h
00004  * \brief Abstract proof rules interface to the simple search engine
00005  * 
00006  * Author: Sergey Berezin
00007  * 
00008  * Created: Mon Feb 24 14:19:48 2003
00009  *
00010  * <hr>
00011  *
00012  * License to use, copy, modify, sell and/or distribute this software
00013  * and its documentation for any purpose is hereby granted without
00014  * royalty, subject to the terms and conditions defined in the \ref
00015  * LICENSE file provided with this distribution.
00016  * 
00017  * <hr>
00018  * 
00019  */
00020 /*****************************************************************************/
00021 
00022 #ifndef _cvc3__search__search_rules_h_
00023 #define _cvc3__search__search_rules_h_
00024 
00025 namespace CVC3 {
00026 
00027   class Theorem;
00028   class Expr;
00029 
00030 /*! \defgroup SE_Rules Proof Rules for the Search Engines
00031  * \ingroup SE
00032  */
00033   //! API to the proof rules for the Search Engines
00034   /*! \ingroup SE_Rules */
00035   class SearchEngineRules {
00036     /*! \addtogroup SE_Rules
00037      * @{ 
00038      */
00039   public:
00040     //! Destructor
00041     virtual ~SearchEngineRules() { }    
00042 
00043     /*! Eliminate skolem axioms: 
00044      * Gamma, Delta |- false => Gamma|- false 
00045      * where Delta is a set of skolem axioms {|-Exists(x) phi (x) => phi(c)}
00046      * and gamma does not contain any of the skolem constants c.
00047      */
00048     virtual Theorem eliminateSkolemAxioms(const Theorem& tFalse, 
00049                const std::vector<Theorem>& delta) = 0;
00050 
00051     // !A |- FALSE ==> |- A
00052     /*! @brief Proof by contradiction: 
00053       \f[\frac{\Gamma, \neg A \vdash\mathrm{FALSE}}{\Gamma \vdash A}\f]
00054     */
00055     /*! \f$\neg A\f$ does not have to be present in the assumptions.
00056      * \param a is the assumption \e A
00057      *
00058      * \param pfFalse is the theorem \f$\Gamma, \neg A \vdash\mathrm{FALSE}\f$
00059      */
00060     virtual Theorem proofByContradiction(const Expr& a,
00061            const Theorem& pfFalse) = 0;
00062 
00063     // A |- FALSE ==> !A
00064     /*! @brief Negation introduction:
00065       \f[\frac{\Gamma, A \vdash\mathrm{FALSE}}{\Gamma\vdash\neg A}\f]
00066      */
00067     /*!
00068      * \param not_a is the formula \f$\neg A\f$.  We pass the negation
00069      * \f$\neg A\f$, and not just \e A, for efficiency: building
00070      * \f$\neg A\f$ is more expensive (due to uniquifying pointers in
00071      * Expr package) than extracting \e A from \f$\neg A\f$.
00072      *
00073      * \param pfFalse is the theorem \f$\Gamma, A \vdash\mathrm{FALSE}\f$
00074      */
00075     virtual Theorem negIntro(const Expr& not_a, const Theorem& pfFalse) = 0;
00076     
00077     // u1:A |- C, u2:!A |- C  ==>  |- C
00078     /*! @brief Case split: 
00079       \f[\frac{\Gamma_1, A\vdash C \quad \Gamma_2, \neg A\vdash C}
00080               {\Gamma_1\cup\Gamma_2\vdash C}\f]
00081      */
00082     /*!
00083      * \param a is the assumption A to split on
00084      *
00085      * \param a_proves_c is the theorem \f$\Gamma_1, A\vdash C\f$
00086      *
00087      * \param not_a_proves_c is the theorem \f$\Gamma_2, \neg A\vdash C\f$
00088      */
00089     virtual Theorem caseSplit(const Expr& a,
00090             const Theorem& a_proves_c,
00091             const Theorem& not_a_proves_c) = 0;
00092 
00093     // Gamma, A_1,...,A_n |- FALSE ==> Gamma |- (OR !A_1 ... !A_n)
00094     /*! @brief Conflict clause rule: 
00095       \f[\frac{\Gamma,A_1,\ldots,A_n\vdash\mathrm{FALSE}}
00096               {\Gamma\vdash\neg A_1\vee\cdots\vee \neg A_n}\f]
00097      */
00098     /*!
00099      * \param thm is the theorem
00100      * \f$\Gamma,A_1,\ldots,A_n\vdash\mathrm{FALSE}\f$
00101      *
00102      * \param lits is the vector of literals <em>A<sub>i</sub></em>.
00103      * They must be present in the set of assumptions of \e thm.
00104      *
00105      * \param gamma FIXME: document this!!
00106      */
00107     virtual Theorem conflictClause(const Theorem& thm,
00108            const std::vector<Theorem>& lits,
00109            const std::vector<Theorem>& gamma) = 0;
00110 
00111     
00112     // "Cut" rule: { G_i |- A_i };  G', { A_i } |- B ==> union(G_i)+G' |- B.
00113     /*! @brief Cut rule:
00114       \f[\frac{\Gamma_1\vdash A_1\quad\cdots\quad\Gamma_n\vdash A_n
00115                 \quad \Gamma', A_1,\ldots,A_n\vdash B}
00116               {\bigcup_{i=1}^n\Gamma_i\cup\Gamma'\vdash B}\f]
00117      */
00118     /*!
00119      * \param thmsA is a vector of theorems \f$\Gamma_i\vdash A_i\f$
00120      *
00121      * \param as_prove_b is the theorem 
00122      *    \f$\Gamma', A_1,\ldots,A_n\vdash B\f$
00123      * (the name means "A's prove B")
00124      */
00125     virtual Theorem cutRule(const std::vector<Theorem>& thmsA,
00126           const Theorem& as_prove_b) = 0;
00127 
00128     // { G_j |- !A_j, j in [1..n]-{i} }
00129     // G |- (OR A_1 ... A_i ... A_n) ==> G, G_j |- A_i
00130     /*! @brief  Unit propagation rule:
00131       \f[\frac{\Gamma_j\vdash\neg A_j\mbox{ for }j\in[1\ldots n]-\{i\}
00132                \quad \Gamma\vdash A_1\vee\cdots\vee A_n}
00133               {\bigcup_{j\in[1\ldots n]-\{i\}}\Gamma_j\cup\Gamma\vdash A_i}\f]
00134      */
00135     /*!
00136      * \param clause is the proof of the clause \f$ \Gamma\vdash
00137      * A_1\vee\cdots\vee A_n\f$
00138      *
00139      * \param i is the index (0..n-1) of the literal to be unit-propagated
00140      *
00141      * \param thms is the vector of theorems \f$\Gamma_j\vdash\neg
00142      * A_j\f$ for all literals except <em>A<sub>i</sub></em>
00143      */
00144     virtual Theorem unitProp(const std::vector<Theorem>& thms,
00145            const Theorem& clause, unsigned i) = 0;
00146     
00147     // { G_j |- !A_j, j in [1..n] } , G |- (OR A_1 ... A_n) ==> FALSE
00148     /*! @brief "Conflict" rule (all literals in a clause become FALSE)
00149       \f[\frac{\Gamma_j\vdash\neg A_j\mbox{ for }j\in[1\ldots n]
00150                \quad \Gamma\vdash A_1\vee\cdots\vee A_n}
00151               {\bigcup_{j\in[1\ldots n]}\Gamma_j\cup\Gamma
00152                \vdash\mathrm{FALSE}}\f]
00153      */
00154     /*!
00155      * \param clause is the proof of the clause \f$ \Gamma\vdash
00156      * A_1\vee\cdots\vee A_n\f$
00157      *
00158      * \param thms is the vector of theorems \f$\Gamma_j\vdash\neg
00159      * A_j\f$
00160      */
00161     virtual Theorem conflictRule(const std::vector<Theorem>& thms,
00162          const Theorem& clause) = 0;
00163 
00164 
00165     // Unit propagation for AND
00166     virtual Theorem propAndrAF(const Theorem& andr_th,
00167              bool left,
00168              const Theorem& b_th) = 0;
00169 
00170     virtual Theorem propAndrAT(const Theorem& andr_th,
00171              const Theorem& l_th,
00172              const Theorem& r_th) = 0;
00173     
00174 
00175     virtual void propAndrLRT(const Theorem& andr_th,
00176            const Theorem& a_th,
00177            Theorem* l_th,
00178            Theorem* r_th) = 0;
00179 
00180     virtual Theorem propAndrLF(const Theorem& andr_th,
00181              const Theorem& a_th,
00182              const Theorem& r_th) = 0;
00183 
00184     virtual Theorem propAndrRF(const Theorem& andr_th,
00185              const Theorem& a_th,
00186              const Theorem& l_th) = 0;
00187 
00188     // Conflicts for AND
00189     virtual Theorem confAndrAT(const Theorem& andr_th,
00190              const Theorem& a_th,
00191              bool left,
00192              const Theorem& b_th) = 0;
00193 
00194     virtual Theorem confAndrAF(const Theorem& andr_th,
00195              const Theorem& a_th,
00196              const Theorem& l_th,
00197              const Theorem& r_th) = 0;
00198 
00199     // Unit propagation for IFF
00200     virtual Theorem propIffr(const Theorem& iffr_th,
00201            int p,
00202            const Theorem& a_th,
00203            const Theorem& b_th) = 0;
00204 
00205     // Conflicts for IFF
00206     virtual Theorem confIffr(const Theorem& iffr_th,
00207            const Theorem& i_th,
00208            const Theorem& l_th,
00209            const Theorem& r_th) = 0;
00210 
00211     // Unit propagation for ITE
00212     virtual Theorem propIterIte(const Theorem& iter_th,
00213         bool left,
00214         const Theorem& if_th,
00215         const Theorem& then_th) = 0;
00216 
00217     virtual void propIterIfThen(const Theorem& iter_th,
00218         bool left,
00219         const Theorem& ite_th,
00220         const Theorem& then_th,
00221         Theorem* if_th,
00222         Theorem* else_th) = 0;
00223 
00224     virtual Theorem propIterThen(const Theorem& iter_th,
00225          const Theorem& ite_th,
00226          const Theorem& if_th) = 0;
00227 
00228     // Conflict for ITE
00229     virtual Theorem confIterThenElse(const Theorem& iter_th,
00230              const Theorem& ite_th,
00231              const Theorem& then_th,
00232              const Theorem& else_th) = 0;
00233 
00234     virtual Theorem confIterIfThen(const Theorem& iter_th,
00235            bool left,
00236            const Theorem& ite_th,
00237            const Theorem& if_th,
00238            const Theorem& then_th) = 0;
00239 
00240     // CNF Rules
00241 
00242     //! AND(x1,...,xn) <=> v  |-  CNF[AND(x1,...,xn) <=> v]
00243     virtual Theorem andCNFRule(const Theorem& thm) = 0;
00244     //! OR(x1,...,xn) <=> v  |-  CNF[OR(x1,...,xn) <=> v]
00245     virtual Theorem orCNFRule(const Theorem& thm) = 0;
00246     //! (x1 => x2) <=> v  |-  CNF[(x1 => x2) <=> v]
00247     virtual Theorem impCNFRule(const Theorem& thm) = 0;
00248     //! (x1 <=> x2) <=> v  |-  CNF[(x1 <=> x2) <=> v]
00249     virtual Theorem iffCNFRule(const Theorem& thm) = 0;
00250     //! ITE(c, x1, x2) <=> v  |-  CNF[ITE(c, x1, x2) <=> v]
00251     virtual Theorem iteCNFRule(const Theorem& thm) = 0;
00252     //! ITE(c, f1, f2) |- (NOT c OR f1) AND (c OR f2)
00253     virtual Theorem iteToClauses(const Theorem& ite) = 0;
00254     //! e1 <=> e2 |- (NOT e1 OR e2) AND (e1 OR NOT e2)
00255     virtual Theorem iffToClauses(const Theorem& iff) = 0;
00256 
00257     virtual Theorem satProof(const Expr& queryExpr, const Proof& satProof) = 0;
00258 
00259     /*! @} */ // end of SE_Rules
00260   }; // end of class SearchEngineRules
00261 
00262 } // end of namespace CVC3
00263 
00264 #endif

Generated on Wed Nov 18 16:13:31 2009 for CVC3 by  doxygen 1.5.2