A prover that decides, depending on the kind of the problem, whether it should try to construct a proof tree or just search for counterexamples
Prover that tries to solve a given problem using a number of different strategies in parallel.
Trait characterising provers, which receive some problem (e.g., from a file) and try to construct a proof, a countermodel, or interpolants
Helper class for storing the sets of declared constants (of various kinds)
and functions, together with the chosen TermOrder
.
Helper class for storing the sets of declared constants (of various kinds)
and functions, together with the chosen TermOrder
.
API that simplifies the use of the prover; this tries to collect various functionality in one place, and provides an imperative API similar to the SMT-LIB command language.
A simple class to simulate commandline calls of Princess from within Java applications.
A collection of tools for analysing and transforming formulae in Presburger arithmetic
Package object making available some of the objects in sub-packages
Package object making available some of the objects in sub-packages
Prover that tries to solve a given problem using a number of different strategies in parallel. Each individual strategy is run using the
IntelliFileProver
class.