Tiziano Dalmonte, Nicola Olivetti, Gian Luca Pozzato, with the valuable help of Cyril Terrioux

HYPNO

Theorem Proving with Hypersequent Calculi for Non-Normal Modal Logics

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

Nonnormal modal logic:    E    EM    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: -
Prolog Code

Logic EM

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

Logic EN

Characterizing axiom: N
box true
Prolog Code

Logic EC

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

Logic EMN

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

Logic EMC

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

Logic ENC

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

Logic EMNC

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

Experiments

Prolog Code for executing tests

The performances of HYPNO seems promising. We have tested it and compared it with PRONOM:

  • 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.

Tests over valid formulas

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 the same system in PRONOM (e.g. e.pl of PRONOM)
  3. consult the Prolog source file of statistics
  4. ask the Prolog engine to prove
    runValidFormulas(+time_limit_in_seconds)

Results

System E
Percentage of timeouts over valid formulas
System \ Timeout 0.1 ms 1 ms 100 ms 1 s 5 s
HYPNO 91,50 % 78,91 % 28,23 % 9,52 % 5,78 %
PRONOM 85,71 % 77,55 % 57,82 % 41,16 % 39,80 %
System EN
Percentage of timeouts over valid formulas
System \ Timeout 0.1 ms 1 ms 100 ms 1 s 5 s
HYPNO 96,60 % 83,67 % 63,27 % 43,88 % 16,19 %
PRONOM 86,05 % 80,27 % 68,57% 57,55% 34,57%
System EM
Percentage of timeouts over valid formulas
System \ Timeout 0.1 ms 1 ms 100 ms 1 s 5 s
HYPNO 92,52 % 75,51 % 26,19 % 7,48 % 5,10 %
PRONOM 85,71 % 77,55 % 60,20 % 31,16 % 19,60 %
System EC
Percentage of timeouts over valid formulas
System \ Timeout 0.1 ms 1 ms 100 ms 1 s 5 s
HYPNO 98,98 % 92,18 % 54,76 % 52,04 % 52,04 %
PRONOM 86,05 % 79,25 % 75,17 % 66,67 % 62,35 %
System EMC
Percentage of timeouts over valid formulas
System \ Timeout 0.1 ms 1 ms 100 ms 1 s 5 s
HYPNO 98,30 % 90,82 % 51,70 % 50,00 % 49,66 %
PRONOM 85,71 % 75,51 % 52,38 % 38,78 % 38,44 %
System ENC
Percentage of timeouts over valid formulas
System \ Timeout 0.1 ms 1 ms 100 ms 1 s 5 s
HYPNO 99,66 % 98,64 % 85,24 % 67,76 % 62,34 %
PRONOM 87,76 % 80,61 % 78,23 % 77,21 % 75,64 %
System EMN
Percentage of timeouts over valid formulas
System \ Timeout 0.1 ms 1 ms 100 ms 1 s 5 s
HYPNO 96,60 % 82,99 % 62,59 % 42,18 % 25,17 %
PRONOM 87,07 % 77,55 % 53,06 % 38,67 % 28,46 %
System EMNC
Percentage of timeouts over valid formulas
System \ Timeout 0.1 ms 1 ms 100 ms 1 s 5 s
HYPNO 99,66 % 98,64 % 84,22 % 77,41 % 43,55 %
PRONOM 86,05 % 79,25 % 61,56 % 41,50 % 38,00 %

Tests over random formulas

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 the same system in PRONOM (e.g. e.pl of PRONOM)
  3. consult the Prolog source file of statistics
  4. ask the Prolog engine to prove
    runRandomFormulas(+number_of_tests,+number_of_propositional_variables,+depth,+time_limit_in_seconds)

Results

System E
Percentage of timeouts over 5000 formulas randomly generated
(For each pair: percentage of timeouts by HYPNO - percentage of timeouts by PRONOM)
Number of propositional variables - Depth 1 ms 10 ms 1 s 10 s
3 vars - depth 5 4 - 5,58 % 0,78 - 1,76 % 0,02 - 0,48 % 0 - 0,22 %
3 vars - depth 7 23,78 - 25,18 % 10,86 - 20,16 % 3,16 - 14,40 % 2,02 - 12 %
7 vars - depth 10 45,22 - 44,94 % 34,36 - 42,36 % 19,06 - 30,30 % 16,06 - %
System EN
Percentage of timeouts over 5000 formulas randomly generated
(For each pair: percentage of timeouts by HYPNO - percentage of timeouts by PRONOM)
Number of propositional variables - Depth 1 ms 10 ms 1 s 10 s
3 vars - depth 5 8,02 - 27,10 % 1,12 - 15,28 % 0,08 - 6,38 % 0,06 - 6,38 %
3 vars - depth 7 40,74 - 58,40 % 16,76 - 48,12% 4,08 - 37,82 % 2,50 - 32,12 %
7 vars - depth 10 73,92 - 81,10 % 56,16 - 77,68 % 35,70 - 56,78 % 23,45 - 34,56 %
System EM
Percentage of timeouts over 5000 formulas randomly generated
(For each pair: percentage of timeouts by HYPNO - percentage of timeouts by PRONOM)
Number of propositional variables - Depth 1 ms 10 ms 1 s 10 s
3 vars - depth 5 4,36 - 7,72 % 1,24 - 3,40 % 0,06 - 0,74 % 0,04 - 0,40 %
3 vars - depth 7 23,36 - 28,84 % 15,62 - 22,82 % 9,18 - 14,56 % 7,68 - 12,35 %
7 vars - depth 10 48,84 - 48,84 % 39,50 - 47,12 % 34,06 - 45,67 % 29,35 - 34,53 %
System EC
Percentage of timeouts over 5000 formulas randomly generated
(For each pair: percentage of timeouts by HYPNO - percentage of timeouts by PRONOM)
Number of propositional variables - Depth 1 ms 10 ms 1 s 10 s
3 vars - depth 5 7,48 - 9,76 % 2,92 - 6,36 % 0,90 - 3,08 % 0,60 - 2,76 %
3 vars - depth 7 30,86 - 31,02 % 19,22 - 25,52 % 12,12 - 23,45 % 8,95 - 19,00 %
7 vars - depth 10 51,66 - 50,00 % 44,18 - 46,92 % 38,28 - 42,67 % 33,45 - 23,79 %
System EMC
Percentage of timeouts over 5000 formulas randomly generated
(For each pair: percentage of timeouts by HYPNO - percentage of timeouts by PRONOM)
Number of propositional variables - Depth 1 ms 10 ms 1 s 10 s
3 vars - depth 5 6,00 - 7,04 % 1,84 - 4,00 % 0,38 - 3,45 % 0,32 - 2,98 %
3 vars - depth 7 28,00 - 27,88 % 19,50 - 22,54 % 12,86 - 19,00 % 8,45 - 12,54 %
7 vars - depth 10 49,76 - 48,56 % 42,64 - 45,12 % 39,56 - 43,34 % 33,41 - 39,00 %
System ENC
Percentage of timeouts over 5000 formulas randomly generated
(For each pair: percentage of timeouts by HYPNO - percentage of timeouts by PRONOM)
Number of propositional variables - Depth 1 ms 10 ms 1 s 10 s
3 vars - depth 5 21,28 - 51,86 % 7,80 - 45,96 % 2,78 - 44,35 % 0,98 - 39,80 %
3 vars - depth 7 56,68 - 68,76 % 36,96 - 62,24% 33,45 - 56,78 % 29,00 - 44,55 %
7 vars - depth 10 21,66 - 50,28 % 70,72 - 80,62 % 56,78 - 67,89 % 38,98 - 49,56 %
System EMN
Percentage of timeouts over 5000 formulas randomly generated
(For each pair: percentage of timeouts by HYPNO - percentage of timeouts by PRONOM)
Number of propositional variables - Depth 1 ms 10 ms 1 s 10 s
3 vars - depth 5 8,34 - 7,38 % 2,68 - 2,22 % 0,48 - 0,46 % 0,20 - 0,24 %
3 vars - depth 7 34,65 - 67,89 % 43,55 - 61,00 % 39,65 - 42,54 % 31,45 - 41,55 %
7 vars - depth 10 65,60 - 52,00 % 61,23 - 49,67 % 54,55 - 48,62 % 39,28 - 42,00 %
System EMNC
Percentage of timeouts over 5000 formulas randomly generated
(For each pair: percentage of timeouts by HYPNO - percentage of timeouts by PRONOM)
Number of propositional variables - Depth 1 ms 10 ms 1 s 10 s
3 vars - depth 5 20,52 - 36,62 % 7,50 - 29,42 % 3,52 - 27,89 % 2,34 - 23,45 %
3 vars - depth 7 58,45 - 55,67 % 55,00 - 49,23 % 42,34 - 43,56 % 30,12 - 38,24 %
7 vars - depth 10 71,67 - 61,34 % 65,89 - 54,60 % 48,00 - 51,83 % 37,77 - 46,36%

Contacts

Authors

Tiziano Dalmonte, Nicola Olivetti, Gian Luca Pozzato

with the valuable help of Cyril Terrioux