Wed, 02/04/2009 - 20:06 — Bilal Said

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

Histto make it different than the accessibility relation labelR. Therootnode 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 theroot).Let

nbe a node andhistits corresponding history node.A formula

<> Ainnis marked as ACTIVE iff (a)Ais not already innand one of the following holds:

- (b1) there exists a formula
[] Binns.t. Done([] B) has not yet been added tohist,- (b2) there is no []-like formulas in
nA formula

<> Amarked as ACTIVE in a nodenyields to create a new successor noden'linked tonby the accessibility relationR. Every[] Bformula innis copied ton'andDone([] B)is added to its history nodehist'. And the conditions (a) (b1) and (b2) guarantee thatn'is notequal toneitherincluded inn, i.e. they guarantee a loop free tableau.

Practically, we apply the following rules in their order:

- propagateNec2ActualWorld
- activatePosWithNec
- activatePosWhenNoNec
- createSuccessors
- 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.