CVC3
Classes | Functions

Proof Rules for the Search Engines

Search Engine
Collaboration diagram for Proof Rules for the Search Engines:

Classes

Functions


Function Documentation

virtual CVC3::SearchEngineRules::~SearchEngineRules ( ) [inline, virtual, inherited]

Destructor.

Definition at line 41 of file search_rules.h.

virtual Theorem CVC3::SearchEngineRules::eliminateSkolemAxioms ( const Theorem tFalse,
const std::vector< Theorem > &  delta 
) [pure virtual, inherited]

Eliminate skolem axioms: Gamma, Delta |- false => Gamma|- false where Delta is a set of skolem axioms {|-Exists(x) phi (x) => phi(c)} and gamma does not contain any of the skolem constants c.

Implemented in CVC3::SearchEngineTheoremProducer.

Referenced by CVC3::SearchImplBase::processResult().

virtual Theorem CVC3::SearchEngineRules::proofByContradiction ( const Expr a,
const Theorem pfFalse 
) [pure virtual, inherited]

Proof by contradiction:

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

.

$\neg A$ does not have to be present in the assumptions.

Parameters:
ais the assumption A
pfFalseis the theorem $\Gamma, \neg A \vdash\mathrm{FALSE}$

Implemented in CVC3::SearchEngineTheoremProducer.

Referenced by CVC3::SearchImplBase::processResult().

virtual Theorem CVC3::SearchEngineRules::negIntro ( const Expr not_a,
const Theorem pfFalse 
) [pure virtual, inherited]

Negation introduction:

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

.

Parameters:
not_ais the formula $\neg A$. We pass the negation $\neg A$, and not just A, for efficiency: building $\neg A$ is more expensive (due to uniquifying pointers in Expr package) than extracting A from $\neg A$.
pfFalseis the theorem $\Gamma, A \vdash\mathrm{FALSE}$

Implemented in CVC3::SearchEngineTheoremProducer.

Referenced by CVC3::SearchImplBase::processResult().

virtual Theorem CVC3::SearchEngineRules::caseSplit ( const Expr a,
const Theorem a_proves_c,
const Theorem not_a_proves_c 
) [pure virtual, inherited]

Case split:

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

.

Parameters:
ais the assumption A to split on
a_proves_cis the theorem $\Gamma_1, A\vdash C$
not_a_proves_cis the theorem $\Gamma_2, \neg A\vdash C$

Implemented in CVC3::SearchEngineTheoremProducer.

virtual Theorem CVC3::SearchEngineRules::conflictClause ( const Theorem thm,
const std::vector< Theorem > &  lits,
const std::vector< Theorem > &  gamma 
) [pure virtual, inherited]

Conflict clause rule:

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

.

Parameters:
thmis the theorem $\Gamma,A_1,\ldots,A_n\vdash\mathrm{FALSE}$
litsis the vector of literals Ai. They must be present in the set of assumptions of thm.
gammaFIXME: document this!!

Implemented in CVC3::SearchEngineTheoremProducer.

Referenced by CVC3::SearchEngineFast::analyzeUIPs().

virtual Theorem CVC3::SearchEngineRules::cutRule ( const std::vector< Theorem > &  thmsA,
const Theorem as_prove_b 
) [pure virtual, inherited]

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}\]

.

Parameters:
thmsAis a vector of theorems $\Gamma_i\vdash A_i$
as_prove_bis the theorem $\Gamma', A_1,\ldots,A_n\vdash B$ (the name means "A's prove B")

Implemented in CVC3::SearchEngineTheoremProducer.

virtual Theorem CVC3::SearchEngineRules::unitProp ( const std::vector< Theorem > &  thms,
const Theorem clause,
unsigned  i 
) [pure virtual, inherited]

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}\]

.

Parameters:
clauseis the proof of the clause $ \Gamma\vdash A_1\vee\cdots\vee A_n$
iis the index (0..n-1) of the literal to be unit-propagated
thmsis the vector of theorems $\Gamma_j\vdash\neg A_j$ for all literals except Ai

Implemented in CVC3::SearchEngineTheoremProducer.

Referenced by CVC3::SearchEngineFast::addNonLiteralFact(), CVC3::Variable::deriveThmRec(), and CVC3::SearchEngineFast::unitPropagation().

virtual Theorem CVC3::SearchEngineRules::conflictRule ( const std::vector< Theorem > &  thms,
const Theorem clause 
) [pure virtual, inherited]

"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}}\]

Parameters:
clauseis the proof of the clause $ \Gamma\vdash A_1\vee\cdots\vee A_n$
thmsis the vector of theorems $\Gamma_j\vdash\neg A_j$

Implemented in CVC3::SearchEngineTheoremProducer.

Referenced by CVC3::SearchEngineFast::addNonLiteralFact(), CVC3::Variable::deriveThmRec(), and CVC3::SearchEngineFast::propagate().

virtual Theorem CVC3::SearchEngineRules::propAndrAF ( const Theorem andr_th,
bool  left,
const Theorem b_th 
) [pure virtual, inherited]
virtual Theorem CVC3::SearchEngineRules::propAndrAT ( const Theorem andr_th,
const Theorem l_th,
const Theorem r_th 
) [pure virtual, inherited]
virtual void CVC3::SearchEngineRules::propAndrLRT ( const Theorem andr_th,
const Theorem a_th,
Theorem l_th,
Theorem r_th 
) [pure virtual, inherited]
virtual Theorem CVC3::SearchEngineRules::propAndrLF ( const Theorem andr_th,
const Theorem a_th,
const Theorem r_th 
) [pure virtual, inherited]
virtual Theorem CVC3::SearchEngineRules::propAndrRF ( const Theorem andr_th,
const Theorem a_th,
const Theorem l_th 
) [pure virtual, inherited]
virtual Theorem CVC3::SearchEngineRules::confAndrAT ( const Theorem andr_th,
const Theorem a_th,
bool  left,
const Theorem b_th 
) [pure virtual, inherited]
virtual Theorem CVC3::SearchEngineRules::confAndrAF ( const Theorem andr_th,
const Theorem a_th,
const Theorem l_th,
const Theorem r_th 
) [pure virtual, inherited]
virtual Theorem CVC3::SearchEngineRules::propIffr ( const Theorem iffr_th,
int  p,
const Theorem a_th,
const Theorem b_th 
) [pure virtual, inherited]
virtual Theorem CVC3::SearchEngineRules::confIffr ( const Theorem iffr_th,
const Theorem i_th,
const Theorem l_th,
const Theorem r_th 
) [pure virtual, inherited]
virtual Theorem CVC3::SearchEngineRules::propIterIte ( const Theorem iter_th,
bool  left,
const Theorem if_th,
const Theorem then_th 
) [pure virtual, inherited]
virtual void CVC3::SearchEngineRules::propIterIfThen ( const Theorem iter_th,
bool  left,
const Theorem ite_th,
const Theorem then_th,
Theorem if_th,
Theorem else_th 
) [pure virtual, inherited]
virtual Theorem CVC3::SearchEngineRules::propIterThen ( const Theorem iter_th,
const Theorem ite_th,
const Theorem if_th 
) [pure virtual, inherited]
virtual Theorem CVC3::SearchEngineRules::confIterThenElse ( const Theorem iter_th,
const Theorem ite_th,
const Theorem then_th,
const Theorem else_th 
) [pure virtual, inherited]
virtual Theorem CVC3::SearchEngineRules::confIterIfThen ( const Theorem iter_th,
bool  left,
const Theorem ite_th,
const Theorem if_th,
const Theorem then_th 
) [pure virtual, inherited]
virtual Theorem CVC3::SearchEngineRules::andCNFRule ( const Theorem thm) [pure virtual, inherited]

AND(x1,...,xn) <=> v |- CNF[AND(x1,...,xn) <=> v].

Implemented in CVC3::SearchEngineTheoremProducer.

Referenced by CVC3::SearchImplBase::applyCNFRules().

virtual Theorem CVC3::SearchEngineRules::orCNFRule ( const Theorem thm) [pure virtual, inherited]

OR(x1,...,xn) <=> v |- CNF[OR(x1,...,xn) <=> v].

Implemented in CVC3::SearchEngineTheoremProducer.

Referenced by CVC3::SearchImplBase::applyCNFRules().

virtual Theorem CVC3::SearchEngineRules::impCNFRule ( const Theorem thm) [pure virtual, inherited]

(x1 => x2) <=> v |- CNF[(x1 => x2) <=> v]

Implemented in CVC3::SearchEngineTheoremProducer.

Referenced by CVC3::SearchImplBase::applyCNFRules().

virtual Theorem CVC3::SearchEngineRules::iffCNFRule ( const Theorem thm) [pure virtual, inherited]

(x1 <=> x2) <=> v |- CNF[(x1 <=> x2) <=> v]

Implemented in CVC3::SearchEngineTheoremProducer.

Referenced by CVC3::SearchImplBase::applyCNFRules().

virtual Theorem CVC3::SearchEngineRules::iteCNFRule ( const Theorem thm) [pure virtual, inherited]

ITE(c, x1, x2) <=> v |- CNF[ITE(c, x1, x2) <=> v].

Implemented in CVC3::SearchEngineTheoremProducer.

Referenced by CVC3::SearchImplBase::applyCNFRules().

virtual Theorem CVC3::SearchEngineRules::iteToClauses ( const Theorem ite) [pure virtual, inherited]

ITE(c, f1, f2) |- (NOT c OR f1) AND (c OR f2)

Implemented in CVC3::SearchEngineTheoremProducer.

Referenced by CVC3::SearchImplBase::enqueueCNFrec().

virtual Theorem CVC3::SearchEngineRules::iffToClauses ( const Theorem iff) [pure virtual, inherited]

e1 <=> e2 |- (NOT e1 OR e2) AND (e1 OR NOT e2)

Implemented in CVC3::SearchEngineTheoremProducer.

Referenced by CVC3::SearchImplBase::applyCNFRules().

virtual Theorem CVC3::SearchEngineRules::satProof ( const Expr queryExpr,
const Proof satProof 
) [pure virtual, inherited]