PolyPaver | Documentation | Changelog
Table of contents
Recent
- Added support for loading conjectures in a modified version of the TPTP formula language.
- Improved pruning of irrelevant hypotheses.
- Eg ignoring the hypothesis \(x + y \leq a\) if the variable \(a\) does not appear anywhere else in the formula.
- Removed support for loading problems specified as Haskell modules.
- Moved to ghc 7.8.4.
PolyPaver 0.2 (2013-05-23)
Linux 32-bit, Windows 32-bit, Haskell source
- Problems can be loaded from .vc files with human friendly syntax.
- Optionally, problems can be loaded from Haskell modules (only if ghc is installed).
- Support for the integral operator.
- New parameter “maximum queue length”. Its default value depends on the selected search mode.
- Variables can be declared to range over integers only.
- By default, PolyPaver now uses DFS and if this fails to decide, PolyPaver automatically runs BFS to search for counter-example near where DFS stopped.
- Proving each conclusion of a Spark VC separately.
- Sorting hypotheses in Spark VCs from smallest to largest.
- Moved from ghc 6.12.3 to ghc 7.4.2.
- Tested on Mac OSX and Windows in addition to Linux 32bit.
PolyPaver 0.1 (2011-09-07):
Linux executable, platform-independent source code
- expressions with explicit intervals and interval operations
- field operations, abs, sqrt, exp, sin, cos
- floating point constants and rounded operations (with adjustable precision)
- solving VCs from SPARK 2005 siv files
- live plotting of pavings for 2D problems (showing which areas of the domain are already proved true and/or showing the location of a counter example)