K + Universal Modalities

A new logic had been added to the library of predefined logics, and it will be integrated in the upcoming minor version release.

In this logic we use different techniques, such as history and model initialization, to optimize the tableau calculus. These techniques are ones of many others offered by LoTREC tableau engine and are needed when implementing an optimized tableau method for some logics such as S5 or PDL.

The logic K + U, where U stands for Universal quantification, consists of:

  • The basic modal logic K: [] phi, <> phi modal operators with krepke semantics
  • With two other operators [U] phi, <U> phi where:
    • M,x |= [U] phi iff All y, M,y |= phi
    • M,x |= <U> phi iff Exists y, M,y |= phi

Semantically, this logic looks like a logic with two modalities 1 and 2:

  • 1 is a K operator
  • 2 is a S5(1) operator, plus the axiom: [2] phi -> [1] phi

(1) Recall, S5 := S4 + B or T + E (i.e. 5)