New in Version 1.8.1 (1 August 2014)
- Look and feel improvements.
- Minor performance enhancements, especially for the QBF preprocessor.
- Proof tree drawing improved.
Version 1.8 (1 March 2013)
- User registration is no longer required.
- New feature: qpro file import.
- New feature: experimental support for GUI-less mode (e.g. without X server).
Usage: java -Djava.awt.headless=true -jar proverbox.jar cmd1 cmd2 ...
where cmd1 cmd2 ... are ProverBox commands as entered on the command prompt.
Commands must be wrapped in quotes if they contain spaces.
Example: java -Djava.awt.headless=true -jar proverbox.jar 'qdimacspreprocess "/tmp/file.qdimacs"'
which runs the QBF preprocessor on the file /tmp/file.qdimacs and is equivalent to
entering qdimacspreprocess "/tmp/file.qdimacs" on the prompt of the ProverBox GUI. - Once again, the QBF preprocessor has been improved.
- The plugin API now includes a library for combinational Boolean circuits.
- The complete plugin API is now using generics.
- Other minor improvements and bugfixes.
- Notice: Java 7 or higher is now required.
Version 1.7 (14 August 2010)
- Once again, the QBF preprocessor has been improved.
- Changes to the plugin API.
Version 1.6 (27 March 2010)
- Significantly improved QBF preprocessor.
- Significantly improved resolution for predicate logic.
Version 1.5.5 (28 January 2010)
- Bugfix for problems with tautologies and free variables in the (Q)DIMACS file import.
Version 1.5.4 (22 September 2009)
- Improved QBF preprocessor.
- New feature: display statistics about QCNF* formulas.
- Bugfix: incorrect QBF preprocessing statistics.
- Bugfix: incorrect handling of files passed on command line.
Version 1.5.3 (21 November 2007)
- New feature: ProverBox is now fully scriptable through the system command line.
- Improved statistics output for QBF preprocessor.
Version 1.5.2 (20 September 2007)
- Improved random formula generator for QHORN.
- Bugfix for QBF preprocessor.
Version 1.5.1 (12 June 2007)
- Improved QBF preprocessor.
Version 1.5 (23 May 2007)
- New feature: QBF preprocessor.
- New feature: universal expansion for QBF*.
- New feature: finding Horn renamings in propositional logic and QBF*.
- Enhancement: additional options for customizing ProverBox.
- Enhancement: ability to suppress large output.
- Bugfix: incorrect frame dimensions at startup.
Version 1.4 (11 December 2006)
- DIMACS and QDIMACS import and export.
- DavisPutnam module: can now prove and solve.
- Internal improvements in handling large formulas.
- Lots of minor enhancements and bugfixes.
Version 1.3.2 (20 January 2006)
- Bugfixes and performance improvements.
Version 1.3.1 (13 December 2005)
- Performance improvements.
Version 1.3 (05 December 2005)
- Random formula generator for QBF*.
- Performance improvements.
- Minor enhancements and bugfixes.
Version 1.2 (01 December 2004)
- New specification language: QBF*.
Version 1.1 (17 June 2004)
- It is now possible to use propositional expressions in predicate logic.
- New license management.
- Preferences dialog added.
- Resolution module: significant performance improvements.
- Minor enhancements and bugfixes.
Version 1.0.6 (18 February 2004)
- Improved Skolemization algorithm.
Version 1.0.5 (15 December 2003)
- Command prompt: tab key allows reusing previous result.
- Minor enhancements and bugfixes.
Version 1.0 (03 September 2003)
- Significantly improved resolution module.
- New option to generate a complete CNF for a propositional formula.
- Davis-Putnam module: a counterexample is provided if a theorem is not provable.
- Improved error handling in command prompt and editor.
- Other minor enhancements and bugfixes.
Version 0.9 (18 August 2003)
- Added proof tree output feature to I/O manager.
- Improved output for resolution module.
- Multithreading: commands can now be executed as independent threads.
- Added Undo / Redo feature to editor.
- Lots of minor enhancements and bugfixes.
Version 0.8 (05 August 2003)
- New formula manager hierarchy.
- Library routines for predicate logic.
- New module: Resolution.
- Support for commands with flags.
- Added "CLS" command, allowing to tidy up the screen.
- Improved help system.
- Automatic declarations now supported by user interface.
Version 0.7 (22 July 2002)
- Specification files now use XML.
- Added parser.
- Implemented language manager.
- Modular architecture for formula and symbol managers.
- New specification language: propositional logic.
- View menu added.
- Project name changed to ProverBox.
- Improved command prompt with support for nested commands.
- Added commands for axiom and theorem handling.
- Improved help system.
- Added predefined types "ANY" and "BOOL".
- Added auto declare.
- Improved plugin API.
- Comfortable user interface for selecting current language and module.
- Added support for formulas in CNF clause-set representation.
- New commands for transforming formulas into propositional normal forms.
- New command: truth tables for propositional formulas.
- Support for embedding components in the output.
- Included sample module: DavisPutnam.
Version 0.6.1 (21 December 2001)
- Bugfixes.
Version 0.6 (19 December 2001)
- Editor added.
- User Settings implemented.
- Command prompt: added command history.
- Working menu bar.
- Optimized resizing behavior.
Version 0.5 (17 July 2001)
- New syntax for declarations.
- Improved handling for the equivalence operator.
Version 0.4 (27 June 2001)
- Formula manager added.
- Command prompt: error reporting improved.
Version 0.3 (24 June 2001)
- Further work on help system.
- Better error reporting when using the command prompt.
- About and version commands added.
- Plugin interface revised.
- Symbol manager now produces sorted output.
- Added simple I/O commands.
Version 0.2 (13 June 2001)
- Help system introduced.
- Symbol manager completed.
- Resource management improved.
- Bugfixes.
Version 0.1 (18 May 2001)
- Symbol manager introduced.