Integrated Logic Software
| The ProverBox is a software environment for logic and automated reasoning: it allows you to transform formulas, determine their satisfiability, automatically prove theorems, and much more.
It provides a modern user interface with a focus on user feedback and visualization. It features an integrated editor and an online help system. |
Open Platform
Modularity and extensibility are among the special features of the ProverBox logic software: multiple logics and multiple theorem proving algorithms are integrated into a common environment.
Advanced users can implement their own algorithms in Java. The ProverBox supports this with a library of data structures and algorithms. In addition, it handles tedious tasks like parsing input and presenting output. | 
|
Out-of-the-Box Experience
The ProverBox currently supports propositional logic, quantified Boolean formulas (QBF) and typed first-order predicate logic.
It includes a resolution prover with advanced strategies like UR-resolution and hyperresolution and a basic DPLL-based propositional satisfiability solver. In addition, it features a novel preprocessor for quantified Boolean formulas.
With just a mouse click, you can switch between the different logics and algorithms!
Explore It!
If you would like to learn more about the ProverBox, please have a look at the Screenshots or browse through the ProverBox Tutorial for a quick overview of the functionality provided by the software. Or even better, Download the ProverBox and see for yourself!
