The Tableau WorkBench (TWB)

A strategy specifies the order in which rules are applied during proof search. The TWB tactic language is inspired by Isabelle tactic language, but note that there are fundamental differences in the undelying model of search.

Let's assume we have defined the following rules for modal logic K as in k_ml_tableau_prover_normal_modal_logic_k : Id , False , And , Or , K . Assume further that t1 and t2 are composite strategies. A strategy is defined using the following operators:

• the basic tactic is a rule and it is identified by a rule name (eg. Id). A rule succeeds if it is applicable;
• The strategies Skip and Fail are two basic strategies that respectively, always succeed or always fail. The strategy Skip is the same as writing a rule that is always applicable and does nothing, the strategy Skip is the same as writing a rule that is never applicable.
• Deterministic alternation, written as t1 ! t2, is the strategy that behaves as t1 if the first rule of t1 is applicable otherwise behaves as t2. If the strategy t1 is selected, the operator ! does not backtrack to choose t2.
• Alternation. Given a node n, the strategy t = t1 | t2, is the strategy that first tries to apply t1 to n. If the result of the visit function, using the strategy t1 is successful, then then t behaves as t1. Otherwise t = t2.
• Sequencing. Given a node n, the strategy t = t1 ; t2 succeed if both t1 and t2 are applicable. Fails otherwise. in particular (t n ) == ( t2 ( t1 n ) )
• Star. Given a node n, the strategy t * behaves as the following expression t* = mu(X) . (t ; X | Skip) , that is, the strategy t is applied as much as possible, and then returns the result of the computation when it fails. Intuitively, if the strategy t suceed m times the result will be t1 ( t2 ( ... ( tm n ) ... ) )


STRATEGY := tactic ( (Id ! False ! And ! Or ! K)* )


Or alternatively:


STRATEGY :=
    let sat = tactic ( (Id ! False ! And ! Or) ) in
    tactic ( ((sat)* ; K )* )


The strategy says ``repeatedly apply the first applicable rule from the left until none are applicable, and then apply the K rule, and repeat this process until no rules are applicable. This strategy is applied to every branch of the proof tree according to the visit algorithm.

More Formally:

't_1 and t_2 are tactics (terms built from this language) and r is a rule: Fail, Skip, Alt(t_1, t_2) (alternation), Rule(r), Seq(t_1, t_2) (sequential application), Repeat(t) (repeatedly apply t''' until it fails, and then succeed).

• Skip: t = Skip : t always succeeds
• Fail: t = Fail : t always fails
• Rule: t = Rule(r) : t succeeds when rule r is applicable.
• AndThen: t = t_1 ; t_2 : t fails if either t_1 or t_2 fail, succeeds otherwise.
• OrElse: t = t_1 | t_2 : t fails if both t_1 and t_2 fail, succeeds otherwise.
• Repeat: Repeat(t) = mu(X) . (t ; X | Skip) : If tactic t succeeds, the tactic Repeat(t) behaves like t ; Repeat(t). If t fails, then the tactic Repeat(t) behaves like Skip. The strategy Repeat always succeeds and is usually written and (t*).