Package edu.udel.cis.vsl.sarl.prove.IF
Module "prove" constitutes the interface between SARL and (possibly external)
theorem provers. It provides an abstract interface
TheoremProver
representing an automated theorem prover as well as implementations for
specific provers (such as CVC3).
The entry-point for using this module is class
Prove. That class provides
static methods for producing instances of
TheoremProverFactory. Those factories are used to produce instances of
TheoremProver.
This package constitutes the public interface for module prove. It provides
interfaces TheoremProver
representing an abstract automated theorem prover, and
TheoremProverFactory representing a factory for producing instances of
TheoremProver. All code
outside of module prove should use only the types defined in this package,
and not any of the implementation packages.
-
ClassDescriptionThis is the entry point for module prove.A data structure that represents the interpretation of a
LogicFunction.Provides an abstract interface for an automated theorem prover operating under a fixed context (i.e., a boolean expression assumed to hold).A factory for producing instances ofTheoremProver.