CVC3
Public Member Functions | List of all members
CVC3::SearchEngineRules Class Referenceabstract

API to the proof rules for the Search Engines. More...

#include <search_rules.h>

Inherited by CVC3::SearchEngineTheoremProducer.

Collaboration diagram for CVC3::SearchEngineRules:
Collaboration graph

Public Member Functions

virtual ~SearchEngineRules ()
 Destructor.
 
virtual Theorem eliminateSkolemAxioms (const Theorem &tFalse, const std::vector< Theorem > &delta)=0
 
virtual Theorem proofByContradiction (const Expr &a, const Theorem &pfFalse)=0
 Proof by contradiction:

\[\frac{\Gamma, \neg A \vdash\mathrm{FALSE}}{\Gamma \vdash A}\]

.

 
virtual Theorem negIntro (const Expr &not_a, const Theorem &pfFalse)=0
 Negation introduction:

\[\frac{\Gamma, A \vdash\mathrm{FALSE}}{\Gamma\vdash\neg A}\]

.

 
virtual Theorem caseSplit (const Expr &a, const Theorem &a_proves_c, const Theorem &not_a_proves_c)=0
 Case split:

\[\frac{\Gamma_1, A\vdash C \quad \Gamma_2, \neg A\vdash C} {\Gamma_1\cup\Gamma_2\vdash C}\]

.

 
virtual Theorem conflictClause (const Theorem &thm, const std::vector< Theorem > &lits, const std::vector< Theorem > &gamma)=0
 Conflict clause rule:

\[\frac{\Gamma,A_1,\ldots,A_n\vdash\mathrm{FALSE}} {\Gamma\vdash\neg A_1\vee\cdots\vee \neg A_n}\]

.

 
virtual Theorem cutRule (const std::vector< Theorem > &thmsA, const Theorem &as_prove_b)=0
 Cut rule:

\[\frac{\Gamma_1\vdash A_1\quad\cdots\quad\Gamma_n\vdash A_n \quad \Gamma', A_1,\ldots,A_n\vdash B} {\bigcup_{i=1}^n\Gamma_i\cup\Gamma'\vdash B}\]

.

 
virtual Theorem unitProp (const std::vector< Theorem > &thms, const Theorem &clause, unsigned i)=0
 Unit propagation rule:

\[\frac{\Gamma_j\vdash\neg A_j\mbox{ for }j\in[1\ldots n]-\{i\} \quad \Gamma\vdash A_1\vee\cdots\vee A_n} {\bigcup_{j\in[1\ldots n]-\{i\}}\Gamma_j\cup\Gamma\vdash A_i}\]

.

 
virtual Theorem conflictRule (const std::vector< Theorem > &thms, const Theorem &clause)=0
 "Conflict" rule (all literals in a clause become FALSE)

\[\frac{\Gamma_j\vdash\neg A_j\mbox{ for }j\in[1\ldots n] \quad \Gamma\vdash A_1\vee\cdots\vee A_n} {\bigcup_{j\in[1\ldots n]}\Gamma_j\cup\Gamma \vdash\mathrm{FALSE}}\]


 
virtual Theorem propAndrAF (const Theorem &andr_th, bool left, const Theorem &b_th)=0
 
virtual Theorem propAndrAT (const Theorem &andr_th, const Theorem &l_th, const Theorem &r_th)=0
 
virtual void propAndrLRT (const Theorem &andr_th, const Theorem &a_th, Theorem *l_th, Theorem *r_th)=0
 
virtual Theorem propAndrLF (const Theorem &andr_th, const Theorem &a_th, const Theorem &r_th)=0
 
virtual Theorem propAndrRF (const Theorem &andr_th, const Theorem &a_th, const Theorem &l_th)=0
 
virtual Theorem confAndrAT (const Theorem &andr_th, const Theorem &a_th, bool left, const Theorem &b_th)=0
 
virtual Theorem confAndrAF (const Theorem &andr_th, const Theorem &a_th, const Theorem &l_th, const Theorem &r_th)=0
 
virtual Theorem propIffr (const Theorem &iffr_th, int p, const Theorem &a_th, const Theorem &b_th)=0
 
virtual Theorem confIffr (const Theorem &iffr_th, const Theorem &i_th, const Theorem &l_th, const Theorem &r_th)=0
 
virtual Theorem propIterIte (const Theorem &iter_th, bool left, const Theorem &if_th, const Theorem &then_th)=0
 
virtual void propIterIfThen (const Theorem &iter_th, bool left, const Theorem &ite_th, const Theorem &then_th, Theorem *if_th, Theorem *else_th)=0
 
virtual Theorem propIterThen (const Theorem &iter_th, const Theorem &ite_th, const Theorem &if_th)=0
 
virtual Theorem confIterThenElse (const Theorem &iter_th, const Theorem &ite_th, const Theorem &then_th, const Theorem &else_th)=0
 
virtual Theorem confIterIfThen (const Theorem &iter_th, bool left, const Theorem &ite_th, const Theorem &if_th, const Theorem &then_th)=0
 
virtual Theorem andCNFRule (const Theorem &thm)=0
 AND(x1,...,xn) <=> v |- CNF[AND(x1,...,xn) <=> v].
 
virtual Theorem orCNFRule (const Theorem &thm)=0
 OR(x1,...,xn) <=> v |- CNF[OR(x1,...,xn) <=> v].
 
virtual Theorem impCNFRule (const Theorem &thm)=0
 (x1 => x2) <=> v |- CNF[(x1 => x2) <=> v]
 
virtual Theorem iffCNFRule (const Theorem &thm)=0
 (x1 <=> x2) <=> v |- CNF[(x1 <=> x2) <=> v]
 
virtual Theorem iteCNFRule (const Theorem &thm)=0
 ITE(c, x1, x2) <=> v |- CNF[ITE(c, x1, x2) <=> v].
 
virtual Theorem iteToClauses (const Theorem &ite)=0
 ITE(c, f1, f2) |- (NOT c OR f1) AND (c OR f2)
 
virtual Theorem iffToClauses (const Theorem &iff)=0
 e1 <=> e2 |- (NOT e1 OR e2) AND (e1 OR NOT e2)
 
virtual Theorem satProof (const Expr &queryExpr, const Proof &satProof)=0
 

Detailed Description

API to the proof rules for the Search Engines.

Definition at line 35 of file search_rules.h.


The documentation for this class was generated from the following file: