Package edu.udel.cis.vsl.sarl.prove.cvc

package edu.udel.cis.vsl.sarl.prove.cvc

This package provides implementations of the TheoremProver and TheoremProverFactory interfaces based on the CVC3 and CVC4 theorem provers. See the CVC3 and CVC4 web pages.

Classes

Class	Description
CVCPowerReal	This is a class provides a PowerReal theory for CVC translator.
CVCTranslator	A CVCTranslator object is used to translate a single symbolic expression to the language of CVC.
RobustCVCTheoremProver	An implementation of TheoremProver using one of the automated theorem provers CVC3 or CVC4.
RobustCVCTheoremProverFactory	Factory for producing new instances of RobustCVCTheoremProver.
Translation	This class is used to deal with integer division or modulo during the CVC translation.