PRONOM A theorem prover for nonnormal modal logics

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

Nonnormal modal logic:    E    EM    EM (opt)    EN    EC    EMN    EMC    ENC    EMNC   





Do NOT use capital letters for propositional variables.
Use: false for bottom, true for top, ^ for conjunction, ? for disjunction, - for negation, -> for material implication, box for modality ▢.

Examples
Valid formulas
  • (box (a ^ (b ? c))) -> (box ((a ^ b) ? (a ^ c)))
  • (box(a ^ b)) -> (box(a)) wwwwwwwwwwwwwwwwiaxiom M
  • box true wwwwwwwwwwwwwwwwwwwwwwwwaxiom N
  • ((box(a)) ^ (box(b))) -> (box(a ^ b)) wwwwwwwwwwiaxiom C
  • b -> (box (a -> a)) wwwwwwwwwwwwwwwwwwwvalid in N


Prolog Source Code

Logic E

Characterizing axiom: -

Logic EM

Characterizing axiom: M
(box(a ^ b)) -> ((box a) ^ (box b))

Logic EN

Characterizing axiom: N
box true

Logic EC

Characterizing axiom: C
((box a) ^ (box b)) -> (box(a ^ b))

Logic EMN

Characterizing axioms: M and N
(box(a ^ b)) -> ((box a) ^ (box b))
box true

Logic EMC

Characterizing axioms: M and C
(box(a ^ b)) -> ((box a) ^ (box b))
((box a) ^ (box b)) -> (box(a ^ b))

Logic ENC

Characterizing axioms: N and C
box true
((box a) ^ (box b)) -> (box(a ^ b))

Logic EMNC

Characterizing axioms: M, N and C
(box(a ^ b)) -> ((box a) ^ (box b))
box true
((box a) ^ (box b)) -> (box(a ^ b))

Experiments

Statistics

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:
  1. consult the Prolog source file of the system to be tested (e.g. e.pl)
  2. consult the Prolog source file of statistics
  3. to run tests over valid formulas, ask the Prolog engine to prove
    runValidFormulas(+time_limit_in_seconds)
  4. 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.


Contacts

Authors

Tiziano Dalmonte, Sara Negri,
Nicola Olivetti, Gian Luca Pozzato

with the valuable help of Cyril Terrioux
  • +39 011 670 68 48
  • gianlucapozzato