Latest News

Since a naive tableau method for S4 may result in an endless loop (e.g. treating naively []<>[] p), we usually add to our method some special techniques in order to guarantee its termination.

In an older version, we have implemented S4 in LoTREC using the loop-test technique. Such as done intuitively on paper, we avoided the endless loops by testing the inclusion of (the set of formulas of) new added nodes in (the set of formulas of) their ancestor nodes. Technically, this requires performing two complex tasks:

  • verifying the ancestor ship of two nodes: searching every ancestor of a node,
  • testing a node inclusion in another node: looking up for every formula in the first node and accessing most of the formulas in the second node.

In this new version, we guarantee the termination using histories. The tableau rules dealing with formulas from the classical logic fragment of S4 are defined similarly. The difference resides in the rules dealing with the [] and <> modalities.

Read more...