# 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)))
valid in E
(box(a ^ b)) >> (box(a))
axiom M
box true
axiom N
((box(a)) ^ (box(b))) >> (box(a ^ b))
axiom C
b >> (box (a >> a))
valid in N

## Prolog Source Code

### For all the systems: Utilities and Operators

To copy in the folder of source files

### 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(+system,+time_limit_in_seconds)
where system can be: e, em, en, ec, enc, emn, emc, emnc
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