An important upgrade of this version of the library is the
integration of the automated theorem prover MetiTarski and the SMT solver Z3 as
external oracles (in collaboration with William Denman, University of Cambridge, UK). This integration is
available through the proof rule
metit. The basic and
classic distributions are "MetiTarski
ready", i.e., these distributions include the proof rule
metit, but the
tools MetiTarski and Z3 have to be installed separately for the
proof rule to work. On the other hand, the full
distribution includes pre-installed binaries of MetiTarski 2.2 and
Z3 4.3.1 for Mac OSX 10.7.3 and higher and 64-bits Linux.
Please, see METIT-LICENSE.txt and
before using these pre-installed binaries.
This version of the library also includes several improvements to
interval_arithmetic. In particular, it
includes support for safe and proper arithmetic operations (as
suggested by Gabor Madl, Honeywell, US) and improved strategies for verifying
properties on real-valued functions. The strategies handle the basic
arithmetic operators (
+,-,*,/), power (
absolute value (
square root (
sqrt), square function (
logarithmic and exponential functions (
irrational constants (
e), strict and
non-strict inequality operators (
##), interval inclusion (
Boolean operators (
not), conditionals (
let-in expressions (
Patches and updates since PVS 6.0 include:
refinement_relations(thanks to Dragan Stosic).
TRS: added confluence theorem for orthogonal rewriting systems (thanks to Ana Cristina Rocha, Andre Galdino, and Mauricio Ayala, Universidade de Brasilia, Brazil).
set_as_list) (thanks to Pierre Neron from Ecole Polytechnique, France).
seq_def.pvssince it duplicates the prelude's type
digraphs: Revisited several definitions and lemmas (thanks to Andreia Avelar and Mauricio Ayala-Rincon from University of Brasilia, Brazil, and Andre Galdino from Federal University of Goias, Brazil).
interval. These strategies are now based on computational reflection and are much more efficient than the previous strategies
skoletinmay generate formulas in a different order. In most cases, the old behavior of
skoletincan be simulated by setting the option
The development Bernstein is still missing in this version of the library. It will be released soon.