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!