S4 with histories

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.

S4-with-loop-test

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. What is achieved by these rules is illustrated as follows:

Once created, every node has one and exactly one history node linked to it by a special relation label Hist to make it different than the accessibility relation label R. The root node has an empty history. The history of each other node will contain all the []-like formulas propagated to it from its ancestor nodes (i.e. the nodes that constitute the path going up to the root).

Let n be a node and hist its corresponding history node.

A formula <> A in n is marked as ACTIVE iff (a) A is not already in n and one of the following holds:

  • (b1) there exists a formula [] B in n s.t. Done([] B) has not yet been added to hist,
  • (b2) there is no []-like formulas in n

A formula <> A marked as ACTIVE in a node n yields to create a new successor node n' linked to n by the accessibility relation R. Every [] B formula in n is copied to n' and Done([] B) is added to its history node hist'. And the conditions (a) (b1) and (b2) guarantee that n' is not equal to neither included in n, i.e. they guarantee a loop free tableau.

S4-with-history

Practically, we apply the following rules in their order:

  1. propagateNec2ActualWorld
  2. activatePosWithNec
  3. activatePosWhenNoNec
  4. createSuccessors
  5. propagateNec

Rule 1. is for axiom T: []p -> p.
Rules 2. and 3. mark the <>-formulas with ACTIVE according to conditions (a) and (b).
Rule 4. creates a successor for each found active <>- formula (if there are any).
Rule 5. copies the []-formulas to the created successors and update their histories. Propagating []-formulas from a node to its successors respects axiom 4 and, altogether with rule 1., it respects axiom K.

This new version helps in reducing the time cost needed to achieve the two complex tasks of loop-test. However, this still need to be proved, as well as the soundness, completeness and termination of the whole method. We will try to provide these proofs later.