In order to test Sibyl for correctness, it has been run on a set of randomly generated tests, and the translations of the same tests into first order logic (using the standard translation of hybrid logic formulae and the straightforward translation of assertions) have then been given in input to the Spass prover (that was run in default mode).
Each test is based on a file generated by HGen (v. 1.2.0). A first group of 1620 tests has been generated using this configuration file for HGen, with modal depth varying from 2 to 10 and, for each modal depth, a number of clauses varying from 10 to 50.
Each file generated by HGen has been modified so as to obtain formulae in the decidable fragment of hybrid logic treated by Sibyl (and, since HGen generated only formulae with direct relations, randomly replacing them with the corresponding converse ones). Moreover, each test has been added a random set of transitivity and inclusion assertion. with 30% probability for a relation to be transitive and 30% probability for any pair of relations R,S to be related by a subrelation assertion.
The tests are grouped in directories according to their modal degree.
Each of such directories contains three subdirectories:
In order to evaluate the impact of the presence of assertions on the
performances of the prover,
from the basic set of tests, other four groups have been obtained
reducing the number of assertions in each file, respectively
to
75%,
50%,
25%
and
no assertions at all.
Such directories are organized similarly to the basic one, but for the
fact that the directory
A table reporting the results of the experiments can be found here.
The so
obtained files are
organized in directories like the tests with the converse
modalities. The subdirectories in each modal depth now include,
beyond
A table reporting the results of the experiments can be found here.
The three provers used for the experiments, Sibyl, SPASS and HTab, have also been run on sets of simple unsatisfiable and satisfiable hand-written problems of regularly increasing difficulty, involving the binder, the global modalities, as well as some easy use of transitivity and relation hierarchies.
The test files are partitioned into two directories,
A table reporting the results of the experiments can be found here.