#include <quant_proof_rules.h>
Inheritance diagram for CVCL::QuantProofRules:
Definition at line 38 of file quant_proof_rules.h.

Destructor.
Definition at line 41 of file quant_proof_rules.h. 

==> NOT EXISTS (vars): e IFF FORALL (vars) NOT e
Implemented in CVCL::QuantTheoremProducer. Referenced by CVCL::TheoryQuant::assertFact(). 

==> NOT FORALL (vars): e IFF EXISTS (vars) NOT e
Implemented in CVCL::QuantTheoremProducer. Referenced by CVCL::TheoryQuant::assertFact(). 

Instantiate a universally quantified formula. From TFORALL(var): e generate Te' where e' is obtained from e by instantiating bound variables with terms in vector<Expr>& terms. The vector of terms should be the same size as the vector of bound variables in e. Also elements in each position i need to have matching types.
Implemented in CVCL::QuantTheoremProducer. Referenced by CVCL::TheoryQuant::recInstantiate(), CVCL::TheoryQuant::semInst(), and CVCL::TheoryQuant::synInst(). 

From T QUANTIFIER (vars): e we get TQUANTIFIER(vars') e where vars' is obtained from vars by removing all bound variables not used in e. If vars' is empty the produced theorem is just Te.
Implemented in CVCL::QuantTheoremProducer. Referenced by CVCL::TheoryQuant::assertFact(). 