by
Tiziano Dalmonte,
Sara Negri,
Nicola Olivetti, and
Gian Luca Pozzato,
with the valuable help of Cyril Terrioux

A Prolog implementation of labelled sequent calculi for logic **E** and standard extensions with **M**, **N**, and **C**

Characterizing axiom: -

Characterizing axiom: M

(box(a ^ b)) -> ((box a) ^ (box b))

Characterizing axiom: N

box true

Characterizing axiom: C

((box a) ^ (box b)) -> (box(a ^ b))

Characterizing axioms: M and N

(box(a ^ b)) -> ((box a) ^ (box b))

box true

Characterizing axioms: M and C

(box(a ^ b)) -> ((box a) ^ (box b))

((box a) ^ (box b)) -> (box(a ^ b))

Characterizing axioms: N and C

box true

((box a) ^ (box b)) -> (box(a ^ b))

Characterizing axioms: M, N and C

(box(a ^ b)) -> ((box a) ^ (box b))

box true

((box a) ^ (box b)) -> (box(a ^ b))

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.

- 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
**runValidFormulas(+time_limit_in_seconds)** - to run tests over randomly generated formulas, ask the Prolog engine to prove
**runRandomFormulas(+number_of_tests,+number_of_propositional_variables,+depth,+time_limit_in_seconds)**

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.

Authors

Nicola Olivetti, Gian Luca Pozzato

with the valuable help of Cyril Terrioux

- +39 011 670 68 48
- gianlucapozzato