1 /*****************************************************************************/ 2 /*! 3 * \file common_proof_rules.h 4 * 5 * Author: Sergey Berezin 6 * 7 * Created: Dec 11 18:15:37 GMT 2002 8 * 9 * <hr> 10 * 11 * License to use, copy, modify, sell and/or distribute this software 12 * and its documentation for any purpose is hereby granted without 13 * royalty, subject to the terms and conditions defined in the \ref 14 * LICENSE file provided with this distribution. 15 * 16 * <hr> 17 * 18 */ 19 /*****************************************************************************/ 20 // CLASS: CommonProofRules 21 // 22 // AUTHOR: Sergey Berezin, 12/09/2002 23 // 24 // Description: Commonly used proof rules (reflexivity, symmetry, 25 // transitivity, substitutivity, etc.). 26 // 27 // Normally, proof rule interfaces belong to their decision 28 // procedures. However, in the case of equational logic, the rules 29 // are so useful, that even some basic classes like Transformer use 30 // these rules under the hood. Therefore, it is made public, and its 31 // implementation is provided by the 'theorem' module. 32 /////////////////////////////////////////////////////////////////////////////// 33 34 #ifndef _cvc3__common_proof_rules_h_ 35 #define _cvc3__common_proof_rules_h_ 36 37 #include <vector> 38 39 namespace CVC3 { 40 41 class Theorem; 42 class Theorem3; 43 class Expr; 44 class Op; 45 46 class CommonProofRules { 47 public: 48 //! Destructor ~CommonProofRules()49 virtual ~CommonProofRules() { } 50 51 //////////////////////////////////////////////////////////////////////// 52 // TCC rules (3-valued logic) 53 //////////////////////////////////////////////////////////////////////// 54 55 // G1 |- phi G2 |- D_phi 56 // ------------------------- 57 // G1,G2 |-_3 phi 58 /*! 59 * @brief Convert 2-valued formula to 3-valued by discharging its 60 * TCC (\f$D_\phi\f$): 61 * \f[\frac{\Gamma_1\vdash_2 \phi\quad \Gamma_2\vdash_2 D_{\phi}} 62 * {\Gamma_1,\,\Gamma_2\vdash_3\phi}\f] 63 */ 64 virtual Theorem3 queryTCC(const Theorem& phi, const Theorem& D_phi) = 0; 65 66 // G0,a1,...,an |-_3 phi G1 |- D_a1 ... Gn |- D_an 67 // ------------------------------------------------- 68 // G0,G1,...,Gn |-_3 (a1 & ... & an) -> phi 69 /*! 70 * @brief 3-valued implication introduction rule: 71 * \f[\frac{\Gamma_0,\,\alpha_1\,\ldots,\,\alpha_n\vdash_3\phi\quad 72 * (\Gamma_i\vdash D_{\alpha_i})_{i\in[1..n]}} 73 * {\Gamma_0,\,\Gamma_1, \ldots, \Gamma_n\vdash_3 74 * (\bigwedge_{i=1}^n\alpha_i)\to\phi}\f] 75 * 76 * \param phi is the formula \f$\phi\f$ 77 * \param assump is the vector of assumptions \f$\alpha_1\ldots\alpha_n\f$ 78 * \param tccs is the vector of TCCs for assumptions 79 * \f$D_{\alpha_1}\ldots D_{\alpha_n}\f$ 80 */ 81 virtual Theorem3 implIntro3(const Theorem3& phi, 82 const std::vector<Expr>& assump, 83 const std::vector<Theorem>& tccs) = 0; 84 85 //////////////////////////////////////////////////////////////////////// 86 // Common rules 87 //////////////////////////////////////////////////////////////////////// 88 89 // ==> u:a |- a 90 //! \f[\frac{}{a\vdash a}\f] 91 virtual Theorem assumpRule(const Expr& a, int scope = -1) = 0; 92 93 // ==> a == a or ==> a IFF a 94 //! \f[\frac{}{a = a}\quad or \quad\frac{}{a \Leftrightarrow a}\f] 95 virtual Theorem reflexivityRule(const Expr& a) = 0; 96 97 //! ==> (a == a) IFF TRUE 98 virtual Theorem rewriteReflexivity(const Expr& a_eq_a) = 0; 99 100 // a1 == a2 ==> a2 == a1 (same for IFF) 101 //! \f[\frac{a_1=a_2}{a_2=a_1}\f] (same for IFF) 102 virtual Theorem symmetryRule(const Theorem& a1_eq_a2) = 0; 103 104 // ==> (a1 == a2) IFF (a2 == a1) 105 //! \f[\frac{}{(a_1=a_2)\Leftrightarrow (a_2=a_1)}\f] 106 virtual Theorem rewriteUsingSymmetry(const Expr& a1_eq_a2) = 0; 107 108 // (a1 == a2) & (a2 == a3) ==> (a1 == a3) [same for IFF] 109 //! \f[\frac{a_1=a_2\quad a_2=a_3}{a_1=a_3}\f] (same for IFF) 110 virtual Theorem transitivityRule(const Theorem& a1_eq_a2, 111 const Theorem& a2_eq_a3) = 0; 112 113 //! Optimized case for expr with one child 114 virtual Theorem substitutivityRule(const Expr& e, const Theorem& thm) = 0; 115 116 //! Optimized case for expr with two children 117 virtual Theorem substitutivityRule(const Expr& e, const Theorem& thm1, 118 const Theorem& thm2) = 0; 119 120 // (c_1 == d_1) & ... & (c_n == d_n) 121 // ==> op(c_1,...,c_n) == op(d_1,...,d_n) 122 /*! @brief 123 \f[\frac{(c_1=d_1)\wedge\ldots\wedge(c_n=d_n)} 124 {op(c_1,\ldots,c_n)=op(d_1,\ldots,d_n)}\f] 125 */ 126 virtual Theorem substitutivityRule(const Op& op, 127 const std::vector<Theorem>& thms) = 0; 128 129 // (c_1 == d_1) & ... & (c_n == d_n) 130 // ==> op(c_1,...,c_n) == op(d_1,...,d_n) 131 /*! @brief 132 \f[\frac{(c_1=d_1)\wedge\ldots\wedge(c_n=d_n)} 133 {op(c_1,\ldots,c_n)=op(d_1,\ldots,d_n)}\f] 134 except that only those arguments are given that \f$c_i\not=d_i\f$. 135 \param e is the original expression \f$op(c_1,\ldots,c_n)\f$. 136 \param changed is the vector of indices of changed kids 137 \param thms are the theorems \f$c_i=d_i\f$ for the changed kids. 138 */ 139 virtual Theorem substitutivityRule(const Expr& e, 140 const std::vector<unsigned>& changed, 141 const std::vector<Theorem>& thms) = 0; 142 virtual Theorem substitutivityRule(const Expr& e, const int changed, const Theorem& thm) = 0; 143 144 // |- e, |- !e ==> |- FALSE 145 /*! @brief 146 \f[\frac{\Gamma_1\vdash e\quad\Gamma_2\vdash \neg e} 147 {\Gamma_1\cup\Gamma_2\vdash \mathrm{FALSE}} 148 \f] 149 */ 150 virtual Theorem contradictionRule(const Theorem& e, 151 const Theorem& not_e) = 0; 152 153 // |- e OR !e 154 virtual Theorem excludedMiddle(const Expr& e) = 0; 155 156 // e ==> e IFF TRUE 157 //! \f[\frac{\Gamma\vdash e}{\Gamma\vdash e\Leftrightarrow\mathrm{TRUE}}\f] 158 virtual Theorem iffTrue(const Theorem& e) = 0; 159 160 // e ==> !e IFF FALSE 161 //! \f[\frac{\Gamma\vdash e}{\Gamma\vdash\neg e\Leftrightarrow\mathrm{FALSE}}\f] 162 virtual Theorem iffNotFalse(const Theorem& e) = 0; 163 164 // e IFF TRUE ==> e 165 //! \f[\frac{\Gamma\vdash e\Leftrightarrow\mathrm{TRUE}}{\Gamma\vdash e}\f] 166 virtual Theorem iffTrueElim(const Theorem& e) = 0; 167 168 // e IFF FALSE ==> !e 169 //! \f[\frac{\Gamma\vdash e\Leftrightarrow\mathrm{FALSE}}{\Gamma\vdash\neg e}\f] 170 virtual Theorem iffFalseElim(const Theorem& e) = 0; 171 172 //! e1 <=> e2 ==> ~e1 <=> ~e2 173 /*! \f[\frac{\Gamma\vdash e_1\Leftrightarrow e_2} 174 * {\Gamma\vdash\sim e_1\Leftrightarrow\sim e_2}\f] 175 * Where ~e is the <em>inverse</em> of e (that is, ~(!e') = e'). 176 */ 177 virtual Theorem iffContrapositive(const Theorem& thm) = 0; 178 179 // !!e ==> e 180 //! \f[\frac{\Gamma\vdash\neg\neg e}{\Gamma\vdash e}\f] 181 virtual Theorem notNotElim(const Theorem& not_not_e) = 0; 182 183 // e1 AND (e1 IFF e2) ==> e2 184 /*! @brief 185 \f[\frac{\Gamma_1\vdash e_1\quad \Gamma_2\vdash(e_1\Leftrightarrow e_2)} 186 {\Gamma_1\cup\Gamma_2\vdash e_2} 187 \f] 188 */ 189 virtual Theorem iffMP(const Theorem& e1, const Theorem& e1_iff_e2) = 0; 190 191 // e1 AND (e1 IMPLIES e2) ==> e2 192 /*! @brief 193 \f[\frac{\Gamma_1\vdash e_1\quad \Gamma_2\vdash(e_1\Rightarrow e_2)} 194 {\Gamma_1\cup\Gamma_2\vdash e_2} 195 \f] 196 */ 197 virtual Theorem implMP(const Theorem& e1, const Theorem& e1_impl_e2) = 0; 198 199 // AND(e_1,...e_n) ==> e_i 200 //! \f[\frac{\vdash e_1\wedge\cdots\wedge e_n}{\vdash e_i}\f] 201 virtual Theorem andElim(const Theorem& e, int i) = 0; 202 203 // e1, e2 ==> AND(e1, e2) 204 /*! @brief 205 \f[\frac{\Gamma_1\vdash e_1\quad \Gamma_2\vdash e_2} 206 {\Gamma_1\cup\Gamma_2\vdash e_1\wedge e_2} 207 \f] 208 */ 209 virtual Theorem andIntro(const Theorem& e1, const Theorem& e2) = 0; 210 211 // e1, ..., en ==> AND(e1, ..., en) 212 /*! @brief 213 \f[\frac{\Gamma_1\vdash e_1\quad \cdots \quad\Gamma_n\vdash e_n} 214 {\bigcup_{i=1}^n\Gamma_i\vdash \bigwedge_{i=1}^n e_i} 215 \f] 216 */ 217 virtual Theorem andIntro(const std::vector<Theorem>& es) = 0; 218 219 // G,a1,...,an |- phi 220 // ------------------------------------------------- 221 // G |- (a1 & ... & an) -> phi 222 /*! 223 * @brief Implication introduction rule: 224 * \f[\frac{\Gamma,\,\alpha_1\,\ldots,\,\alpha_n\vdash\phi} 225 * {\Gamma\vdash(\bigwedge_{i=1}^n\alpha_i)\to\phi}\f] 226 * 227 * \param phi is the formula \f$\phi\f$ 228 * \param assump is the vector of assumptions \f$\alpha_1\ldots\alpha_n\f$ 229 */ 230 virtual Theorem implIntro(const Theorem& phi, 231 const std::vector<Expr>& assump) = 0; 232 233 //! e1 => e2 ==> ~e2 => ~e1 234 /*! \f[\frac{\Gamma\vdash e_1\Rightarrow e_2} 235 * {\Gamma\vdash\sim e_2\Rightarrow\sim e_1}\f] 236 * Where ~e is the <em>inverse</em> of e (that is, ~(!e') = e'). 237 */ 238 virtual Theorem implContrapositive(const Theorem& thm) = 0; 239 240 //! ==> ITE(TRUE, e1, e2) == e1 241 virtual Theorem rewriteIteTrue(const Expr& e) = 0; 242 //! ==> ITE(FALSE, e1, e2) == e2 243 virtual Theorem rewriteIteFalse(const Expr& e) = 0; 244 //! ==> ITE(c, e, e) == e 245 virtual Theorem rewriteIteSame(const Expr& e) = 0; 246 247 // NOT e ==> e IFF FALSE 248 //! \f[\frac{\vdash\neg e}{\vdash e\Leftrightarrow\mathrm{FALSE}}\f] 249 virtual Theorem notToIff(const Theorem& not_e) = 0; 250 251 // e1 XOR e2 ==> e1 IFF (NOT e2) 252 //! \f[\frac{\vdash e_1 XOR e_2}{\vdash e_1\Leftrightarrow(\neg e_2)}\f] 253 virtual Theorem xorToIff(const Expr& e) = 0; 254 255 //! ==> (e1 <=> e2) <=> [simplified expr] 256 /*! Rewrite formulas like FALSE/TRUE <=> e, e <=> NOT e, etc. */ 257 virtual Theorem rewriteIff(const Expr& e) = 0; 258 259 // AND and OR rewrites check for TRUE and FALSE arguments and 260 // remove them or collapse the entire expression to TRUE and FALSE 261 // appropriately 262 263 //! ==> AND(e1,e2) IFF [simplified expr] 264 virtual Theorem rewriteAnd(const Expr& e) = 0; 265 266 //! ==> OR(e1,...,en) IFF [simplified expr] 267 virtual Theorem rewriteOr(const Expr& e) = 0; 268 269 //! ==> NOT TRUE IFF FALSE 270 virtual Theorem rewriteNotTrue(const Expr& e) = 0; 271 272 //! ==> NOT FALSE IFF TRUE 273 virtual Theorem rewriteNotFalse(const Expr& e) = 0; 274 275 //! ==> NOT NOT e IFF e, takes !!e 276 virtual Theorem rewriteNotNot(const Expr& e) = 0; 277 278 //! ==> NOT FORALL (vars): e IFF EXISTS (vars) NOT e 279 virtual Theorem rewriteNotForall(const Expr& forallExpr) = 0; 280 281 //! ==> NOT EXISTS (vars): e IFF FORALL (vars) NOT e 282 virtual Theorem rewriteNotExists(const Expr& existsExpr) = 0; 283 284 //From expr EXISTS(x1: t1, ..., xn: tn) phi(x1,...,cn) 285 //we create phi(c1,...,cn) where ci is a skolem constant 286 //defined by the original expression and the index i. 287 virtual Expr skolemize(const Expr& e) = 0; 288 289 /*! skolem rewrite rule: Introduces axiom |- Exists(x) phi(x) <=> phi(c) 290 * where c is a constant defined by the expression Exists(x) phi(x) 291 */ 292 virtual Theorem skolemizeRewrite(const Expr& e) = 0; 293 294 //! Special version of skolemizeRewrite for "EXISTS x. t = x" 295 virtual Theorem skolemizeRewriteVar(const Expr& e) = 0; 296 297 //! |- EXISTS x. e = x 298 virtual Theorem varIntroRule(const Expr& e) = 0; 299 300 /*! @brief If thm is (EXISTS x: phi(x)), create the Skolemized version 301 and add it to the database. Otherwise returns just thm. */ 302 /*! 303 * \param thm is the Theorem(EXISTS x: phi(x)) 304 */ 305 virtual Theorem skolemize(const Theorem& thm) = 0; 306 307 //! Retrun a theorem "|- e = v" for a new Skolem constant v 308 /*! 309 * This is equivalent to skolemize(d_core->varIntroRule(e)), only more 310 * efficient. 311 */ 312 virtual Theorem varIntroSkolem(const Expr& e) = 0; 313 314 // Derived rules 315 316 //! ==> TRUE 317 virtual Theorem trueTheorem() = 0; 318 319 //! AND(e1,e2) ==> [simplified expr] 320 virtual Theorem rewriteAnd(const Theorem& e) = 0; 321 322 //! OR(e1,...,en) ==> [simplified expr] 323 virtual Theorem rewriteOr(const Theorem& e) = 0; 324 325 // TODO: do we really need this? 326 virtual std::vector<Theorem>& getSkolemAxioms() = 0; 327 328 //TODO: do we need this? 329 virtual void clearSkolemAxioms() = 0; 330 331 virtual Theorem ackermann(const Expr& e1, const Expr& e2) = 0; 332 333 // Given a propositional atom containing embedded ite's, lifts first ite condition 334 // to form a Boolean ITE 335 // |- P(...ite(a,b,c)...) <=> ite(a,P(...b...),P(...c...)) 336 virtual Theorem liftOneITE(const Expr& e) = 0; 337 338 }; // end of class CommonProofRules 339 340 } // end of namespace CVC3 341 342 #endif 343