CVC3  2.4.1
common_proof_rules.h
Go to the documentation of this file.
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 
47  public:
48  //! Destructor
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
virtual Theorem iffNotFalse(const Theorem &e)=0
Data structure of expressions in CVC3.
Definition: expr.h:133
virtual Theorem rewriteNotExists(const Expr &existsExpr)=0
==> NOT EXISTS (vars): e IFF FORALL (vars) NOT e
virtual Theorem assumpRule(const Expr &a, int scope=-1)=0
virtual Theorem rewriteAnd(const Expr &e)=0
==> AND(e1,e2) IFF [simplified expr]
virtual Theorem iffFalseElim(const Theorem &e)=0
virtual Theorem reflexivityRule(const Expr &a)=0
virtual Theorem3 queryTCC(const Theorem &phi, const Theorem &D_phi)=0
Convert 2-valued formula to 3-valued by discharging its TCC ( ): .
virtual Theorem implContrapositive(const Theorem &thm)=0
e1 => e2 ==> ~e2 => ~e1
virtual Theorem rewriteNotFalse(const Expr &e)=0
==> NOT FALSE IFF TRUE
virtual Expr skolemize(const Expr &e)=0
virtual Theorem rewriteNotNot(const Expr &e)=0
==> NOT NOT e IFF e, takes !!e
virtual Theorem excludedMiddle(const Expr &e)=0
virtual Theorem notToIff(const Theorem &not_e)=0
virtual Theorem rewriteIteFalse(const Expr &e)=0
==> ITE(FALSE, e1, e2) == e2
Theorem3.
Definition: theorem.h:308
virtual Theorem implMP(const Theorem &e1, const Theorem &e1_impl_e2)=0
virtual Theorem contradictionRule(const Theorem &e, const Theorem &not_e)=0
virtual Theorem iffTrue(const Theorem &e)=0
virtual Theorem skolemizeRewrite(const Expr &e)=0
virtual Theorem substitutivityRule(const Expr &e, const Theorem &thm)=0
Optimized case for expr with one child.
virtual Theorem implIntro(const Theorem &phi, const std::vector< Expr > &assump)=0
Implication introduction rule: .
virtual std::vector< Theorem > & getSkolemAxioms()=0
virtual Theorem rewriteIteSame(const Expr &e)=0
==> ITE(c, e, e) == e
virtual Theorem skolemizeRewriteVar(const Expr &e)=0
Special version of skolemizeRewrite for "EXISTS x. t = x".
virtual Theorem andIntro(const Theorem &e1, const Theorem &e2)=0
virtual ~CommonProofRules()
Destructor.
virtual Theorem rewriteIteTrue(const Expr &e)=0
==> ITE(TRUE, e1, e2) == e1
virtual void clearSkolemAxioms()=0
virtual Theorem trueTheorem()=0
==> TRUE
virtual Theorem3 implIntro3(const Theorem3 &phi, const std::vector< Expr > &assump, const std::vector< Theorem > &tccs)=0
3-valued implication introduction rule:
virtual Theorem rewriteNotForall(const Expr &forallExpr)=0
==> NOT FORALL (vars): e IFF EXISTS (vars) NOT e
virtual Theorem xorToIff(const Expr &e)=0
virtual Theorem liftOneITE(const Expr &e)=0
virtual Theorem transitivityRule(const Theorem &a1_eq_a2, const Theorem &a2_eq_a3)=0
(same for IFF)
virtual Theorem iffContrapositive(const Theorem &thm)=0
e1 <=> e2 ==> ~e1 <=> ~e2
virtual Theorem rewriteReflexivity(const Expr &a_eq_a)=0
==> (a == a) IFF TRUE
virtual Theorem rewriteIff(const Expr &e)=0
==> (e1 <=> e2) <=> [simplified expr]
virtual Theorem rewriteUsingSymmetry(const Expr &a1_eq_a2)=0
virtual Theorem varIntroRule(const Expr &e)=0
|- EXISTS x. e = x
virtual Theorem iffMP(const Theorem &e1, const Theorem &e1_iff_e2)=0
virtual Theorem notNotElim(const Theorem &not_not_e)=0
Definition: expr.cpp:35
virtual Theorem ackermann(const Expr &e1, const Expr &e2)=0
virtual Theorem symmetryRule(const Theorem &a1_eq_a2)=0
(same for IFF)
virtual Theorem varIntroSkolem(const Expr &e)=0
Retrun a theorem "|- e = v" for a new Skolem constant v.
virtual Theorem rewriteNotTrue(const Expr &e)=0
==> NOT TRUE IFF FALSE
virtual Theorem rewriteOr(const Expr &e)=0
==> OR(e1,...,en) IFF [simplified expr]
virtual Theorem andElim(const Theorem &e, int i)=0
virtual Theorem iffTrueElim(const Theorem &e)=0