Tests over valid formulas and over random formulas
The performances of PRONOM seems prmising. We have tested it:
- on sets of valid formulas for each modal logic
- on sets of randomly generated formulas, obtained by fixing the number of propositional variables,
the depth (level of nesting of connectives) of a formula and a time limit.
To run tests:
- consult the Prolog source file of the system to be tested (e.g. e.pl)
- consult the Prolog source file of statistics
- to run tests over valid formulas, ask the Prolog engine to prove
- to run tests over randomly generated formulas, ask the Prolog engine to prove
Results of tests over valid formulas are shown in Table 1, whereas the percentage
of timeouts in executing tests over randomly generated formulas are shown in Table 2.
Table 1: percentage of timeouts of PRONOM over N valid formulas, 90 < N < 500.
Table 2: percentage of timeouts of PRONOM over 8000 formulas randomly generated.