Benchmarks
From BWare
(Difference between revisions)
| Line 7: | Line 7: | ||
In this release, several formats are proposed and are divided into several archives. The considered formats are the following: | In this release, several formats are proposed and are divided into several archives. The considered formats are the following: | ||
| − | * TPTP FOF format: this is the regular TPTP format for mono-sorted first order logic; | + | * [[Media:BWare_PO_v1_FOF.tgz|TPTP FOF format]]: this is the regular TPTP format for mono-sorted first order logic; |
* TPTP FOF TFF1 format: this is the TPTP format for first order logic with polymorphic types (à la ML); | * TPTP FOF TFF1 format: this is the TPTP format for first order logic with polymorphic types (à la ML); | ||
* SMT-LIB v2 format: this is the regular SMT format for many-sorted first order logic; | * SMT-LIB v2 format: this is the regular SMT format for many-sorted first order logic; | ||
Revision as of 19:10, 11 March 2015
Release v1
This is the release v1 of the B Proof Obligation (PO) benchmark of the BWare project. This release is under the CeCILL-B license, and consists of a set of 12,876 POs, which has been provided by ClearSy and Mitsubishi Electric R&D Centre Europe, two industrial partners of the BWare project.
In this release, several formats are proposed and are divided into several archives. The considered formats are the following:
- TPTP FOF format: this is the regular TPTP format for mono-sorted first order logic;
- TPTP FOF TFF1 format: this is the TPTP format for first order logic with polymorphic types (à la ML);
- SMT-LIB v2 format: this is the regular SMT format for many-sorted first order logic;
- Alt-Ergo native format: this is the input format of Alt-Ergo.
For further information regarding this release, please read the documentation file here.
Before using this benchmark, carefully read the licensing agreement (included in each archive).
