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.

  • Class
    This 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 of TheoremProver.