The following notions would be useful for understanding some of the more advanced concepts: termination methods like loop-checks and histories; optimisation methods like backjumping and simplification; proof-theoretic notions like invertible rules, contracton-free calculi and stoups.
The TWB provides an extremely simple way for specifying the syntax of formulae and rules, together with a simple way to specify a search strategy for rule applications. It provides basic facilities for ensuring termination via loop checks (blocking) and also allows information to be passed from children to parents using variables. There are also hooks which allow you to implement more complicated optimisation techniques like backjumping (use-check) and (modal) simplification.
The underlying implementation uses high-level functional programming to avoid imperative constructs, and is tuned for efficiency. For example, our optimised implementation of modal logic K is competitive against the Logics Work Bench. The TWB currently has implementations tableau/sequent provers for the following propositional logics: CPL, K, KT, S4, PLTL, UB, LCK, CTL. We plan to add the following soon: K4, K45, S5, G, Grz, PDL, Int, BiInt, Kt, Kt.S4 ...
We explain the basic architecture of the TWB, give pointers to the theory underlying this architecture, and then concentrate on how to build tableau-based and sequent-based theorem provers for various propositional non-classical logics using case-studies and exercises.
We now discuss several aspects of tableau calculi which are important when trying to mechanize the tableau method. We assume the reader is familiar with tableau methods.
Tableau rules are of the form N ----------- d1 ... dn where N is the numerator, while d1 ... dn is a list of n denominators. The numerator contains one or more distinguished formula schemas called principal formulae and one or more formulae schema called side formulae. We use meta-variables A, B, P, Q, ... to represent principal formulae and X,Y,Z for, possibly empty, "containers" of side formulae: traditionally sets, multisets or sequences, but possibly more complex data structures for generality.
Operationally, tableau rules can be seen as functions to transform a (container) node into a list of (container) nodes during the construction of a graph. We say that a rule is applicable if we can partition the contents of the current node to instantiate the meta-variables in the numerator . The denominators of a rule represent actions to expand the graph by creating new nodes according to these instantiations.
The repeated application of rules gives rise to a tree of nodes, with children obtained from their parent by instantiating a rule. To capture sequent calculi as well as tableau calculi, we view this process as a search for a proof where all leaves are "closed". But in general, for tableau calculi with cyclic proofs, there are really three notions: success, failure and undetermined: we stay with the dichotomy "closed" as success (of proof search) and "open" as failure (of proof search) for now to simplify the exposition.
A numerator pattern like Z is unrestricted since its shape does not restrict its contents in any way. Conversely, the pattern Box X is restricted to contain only Box-formulae, X &Y is restricted to contain only &-formulae while {A & B} is restricted to contain exactly one single &-formula. Patterns like X & Y are allowed to be empty, but {A & B} is not.
Currently, we forbid purely structural numerators like X;Y which non-determ-inistically partition the node N into two arbitrary disjoint containers X and Y (even though such numerators may be useful for linear logic), and numerators like Box X ; Box Y; Z since both can lead to an exponential number of possible different partitions.
Consequently, the only form of non-determinism in rules is the formula choice non-determinism in choosing the principal formula. More generally called instance choice, this non-determinism leads to implicit branching since the choice-point is hidden in the pattern-matching (rule instance). We return to this issue later after identifying the various forms of non-determinism inherent in tableau proof search.
The TWB is organised into four main components which total roughly 4000 lines of Ocaml code (loc). The core (464 loc) contains all type definitions and the strategy implementation. The data-type library (664 loc) implements support data structures. The tableau library (818) provides the machinery to implement tableau-based provers. The syntax library (1624) provides an easy way to access the TWB library and to define specific logic modules. Finally the command line interface (226 loc) provides a simple shell interface for compiling and executing the logic modules on input formulae.
The core library defines the architecture of the prover using abstract data types. The core library is composed of the following modules:
[inline:algorithm.gif]
The core algorithm of the TWB is a procedure to visit a tree that is generated by the repeated application of a finite set of rules to an initial node containing a finite number of formulae.
The visit procedure is basically an interpreter for the strategy language. Given the state of the strategy and the current node returns the result of the visit of the tree generated by applying the strategy to the current node. The strategy embedes the tableau/sequent rule to be applied following the specification language in defining_strategy. In principle, the end result of the visit procedure is a list of results as the alt operator of the strategy effectively is a branching operator at the strategy level. However, since the alt operator is always guarded by an acceptance condition, only one result is selected from a strategy even when both alternations are equally applicable.
In the figure above, we show a snapshot of the visit procedure by focusing on a node in the proof tree (the current node).
A don't care non-deterministic choice is an arbitrary choice of one among multiple possible continuations for a computation, all of which return the same result. A don't know non-deterministic choice is one choice among multiple possible continuations, which do not necessarily return the same result. For completeness in a tableau calculus, it is sufficient to assume that all choices are don't know non-deterministic. However, a deterministic algorithm based on this assumption will be extremely inefficient since it has to consider all possible continuations for all choices. Thus it is imperative to remove as many forms of non-determinism as possible.
Traditionally, logicians focus on the existence of a derivation tree rather than on how it is found. Conversely, automated reasoners focus on designing algorithms to search for a derivation tree as efficiently as possible. From a theoretical perspective, it is therefore not important to specify the order in which rules are applied or how the proof tree is explored.
Practically, however, specifying a particular rule order can dramatically speed up the search and construction of a proof tree. Moreover, since different rule orders can produce different derivation trees, an efficient decision procedure should always try to build the smallest derivation tree. In general, we can identify three forms of non-determinism associated with three fundamental aspects of a generic decision procedure:
For example, in classical propositional logic, where all rules are invertible, the order in which rules are applied is not important. However specifying a strategy that applies all linear rules and the axiom first, and then all branching rules, can potentially shorten the proof tree. The problem is however different in basic modal logic, where not all sequences of rule applications ensure a solution since the (K)-rule is not invertible.
The problem is even more complicated in tableau-sequent calculi with more than one non-invertible rule: for example intuitionistic logic. In this situation, at any given choice point, after all invertible rules are applied, we are forced to guess which non-invertible rule to apply, and eventually to undo this decision if it does not lead to the construction of an acceptable proof tree. Consequently, if the proof tree obtained from the application of the first rule of a sequence of non-invertible rules does not respect a logic-specific condition, the entire proof tree generated from that rule application must be discarded. To recover from this wrong choice, the proof must be re-started using the next non-invertible rule available in the sequence. Thus, for efficiency, tableau rules must be coupled with a strategy to control the order in which rules are applied.
The underlying engine contains a backtracking procedure which is turned on as soon as a closed node is found and as soon as no rule is applicable to a node.
Each of the three forms of non-determinism give rise to And-branching. That is: - choosing different current nodes will give rise to different tableaux; - choosing different rules to apply to the current node will give rise to different tableaux; - choosing different principal formulae for the chosen rule and the chosen node will give rise to different tableaux.
But we need only one of these tableaux to close.
Thus we have the following backtracking principle: backtrack over all choice points until we find a tableau such that each And-node has at least one closed child and each Or-node has all children closed.
At any stage, if the backtracking algorithm finds a closed tableau, then it stop backtracking and simply returns closed.
Conversely, as long as it fails to find a closed tableau, it continues to backtrack over all choice points.
Thus, on the way down, strategies tell us how to construct the current tableau and how to leave And- and Or- choice points in creating the tableau.
During backtracking, some of these choice-points are activated, as long as we have not found a closed tableau.
The TWB has the infrastructure to add histories and variables to tableau/sequent rules. Operationally, a history or a variable is an object that must be instantiated by the user when defining a logic module.
The TWB library defines the interface for such objects in terms of an Ocaml functor. The TWB data types library defines three generic data structures that can be assembled by the user to define complex histories or variables. The three basic functors to build such data structures are:
A functor is a function that given a module of type ElementTYPE returns a module of type TwbSet.S . The ElementTYPE type module has the follwing signature:
module type ValType = sig type t val copy : t -> t val to_string : t -> string end
For example, if we want to add a history of type set of formulae we need to define a module FormulaSet by using the functor TwbSet.Make and passing to it the type formula as ElementTYPE as shown below.
module FormulaSet = TwbSet.Make( struct type t = formula let to_string = formula_printer let copy s = s end )
Once the module is defined, we add it to the tableau/sequent node by using the following syntax. The keyword HISTORIES expects a sequence of history declarations. Each such declaration consists of three elements. The first element is an uppercase identifier (e.g. BOXES) naming the history used in the tableau rules, followed by a colon. The second element is the type of the history (e.g FormulaSet.Set) , followed by an := operator. The third element is the default value for the history (e.g. a new empty object of type FormulaSet.set).
HISTORIES BOXES : FormulaSet.set := new FormulaSet.set END
Variables are declared similarly with the following syntax. The only difference is that the identifier used for variables is always lowercase. VARIABLES var1 : FormulaSet.set := new FormulaSet.set END
class type ['basetype] twbset = object('typesettype) method add : 'basetype -> 'typesettype method add_filter : ('basetype -> 'basetype -> bool ) -> 'basetype -> 'typesettype method addlist : 'basetype list -> 'typesettype method del : 'basetype -> 'typesettype method mem : 'basetype -> bool method elements : 'basetype list method hd : 'basetype method is_empty : bool method filter : ('basetype -> bool) -> 'typesettype method length : int method cardinal : int method intersect : 'typesettype -> 'typesettype method union: 'typesettype -> 'typesettype method subset: 'typesettype -> bool method is_equal : 'typesettype -> bool method copy : 'typesettype method empty : 'typesettype method to_string : string end
The TwbSet API is parametrized in the its input type. In the following let 'basetype be the base type (eg. a formula or a Formula.set ) and 'twbsettype the resulting type TwbSet.set . We now explain all methods
Example: (* add : (formula list * Formula.set) -> Formula.set *) let add (l,h) = h#addlist l
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:
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).
In the first part of this tutorial we are introducing the tableau workbech by means of a small example based on classical propositional logic. We give the the for the calculus, both in tableau and sequent notation and we show a simple negation normal form function. Then we show how to run the TWB from the command line and how to trace the proof.
Each file in the TWB are translated in an Ocaml compilation unit. We assume that the logic rules for the propositional modal logic shown before are saved in a file pc.ml and the negation normal form function in a file pclib.ml . To compile the logic module we use the utility twbcompile that is shipped with the TWB libraries.
$./twbcompile pc.ml ............Done. $
The result of the compilation is the file pc.twb that is the object prover for propositional classical logic.
To run the file pc.twb we can either give it a file of formulae to prove as argument or passing a formula on the stdin channel.
We show the proof trace of a simple tautology ~ (~ p) <-> p: $./pc.twb --trace ~ (~ p) <-> p Proving: ~ (~ p) <-> p Start Node: ((p & (~ p)) v (p & (~ p))) Or ( 0 -> 1 ) (p & (~ p)) ; And ( 1 -> 2 ) (~ p) ; p Id ( 2 -> 3 ) Or ( 0 -> 4 ) (p & (~ p)) ; And ( 4 -> 5 ) (~ p) ; p Id ( 5 -> 6 ) Time:0.0000 Result:Close Total Rules applications:6
'Note that the initial formula is immediately transformed into negated normal form before being processed by the tableau rules.'
Provers generated with the TWB have a number of standard options to switch on/off different behaviors. In particular, for the moment we concentrate on just a few of the options :
the prover is used as a satisfiability procedure. The same effect is obtained by not specifying a value for the NEG function in the logic module source.
is the pre-processing function PP.
is possible to do a step by step analysis of the proof. Useful for debugging.
$./pc.twb --help usage: ./pc.twb [-options] [file] --nopp disable preproc function --noneg disable negation function --level trace level --trace print proof trace --time set exec timeout --verbose print additional information --outdir set output directory --out set output type --nocache disable function memoization -help Display this list of options --help Display this list of options
CONNECTIVES [ "~";"&";"v";"->";"<->" ]
The keyword CONNECTIVES in the TWB introduces a list of string separated with a simicolon ";". Each string can be used as a connective in the grammar definition (below) and it will become a reserved keyword. Connectives can be of variable length, can be composed by a mix of numbers, symbols and characters.
GRAMMAR formula := ATOM | Verum | Falsum | formula & formula | formula v formula | formula -> formula | formula <-> formula | ~ formula ;; expr := formula ;; END
The TWB allows the user to define the grammar to be used for the formulae in the tableau/sequent rules. A TWB grammar is composed of a sequence of productions separated by a double semicolon ";;". Two mandatory productions are formula and expr. A third pre-defined production that can be omitted is node.
At the moment of writing the grammar machinery still has some minor bugs that we are seeking to address in future releases.
open Twblib open Pclib
Since the TWB is built on top of ocaml, it is possible to specify arbitrary ocaml functions with a twb file. In this example, we use twb modules by using the ocaml directive open. This operation imports into the current namespace all the functions and data types defined in the module "twblib.ml" and "pclib.ml".
Note that the leading lowercase letter of the file name is capitalised when using the "open" directive.
In general, it is possible to write arbitrary functions and data types that can be used in the subsequent part of file.
TABLEAU RULE Id { a } ; { ~ a } ; X === Close END RULE False { Falsum} ; X === Close END RULE And { A & B } ; X === A ; B ; X END RULE Or { A v B } ; X === A ; X | B ; X END END
A tableau definition is delimited of the keywords TABLEAU ... END. A tableau is composed of a sequence of rule definitions. A rule is delimited by the keywords RULE ... END . In general, tableau/sequent rules may consist of up to seven components:
RULE False { Falsum } ; X ======================= Close END
This rule define an axiom. The rule is introduced by the keyword RULE, it is the followed by an uppercase rule identifier False that will be used to invoke the rule in the strategy section. The body of the rule is a schema representing a tableau / sequent node as defined in the grammar. In this case a tableau node is a set of formulae separated by a semicolon ";". In this case, for the rule to be applicable, the node schema requires a principal formula containing the constant Falsum and an anonymous, possibly empty, set of formulae X that contains all other formulae in the node.
If the rule is applicable, then this particular rule stops the procedure by using the keyword Close. Intuitively this rule is a device to stop the procedure whenever we find an instance of bottom (Falsum) in the tableau node.
RULE Id { a } ; { ~ a } ; X ========================= Close END
The rule above defines the axiom Id that detects classical inconsistencies, that is a positive and a negative occurrence of an atom in a tableau node. The body of this rule has two principal formulae and a anonymous set X. This rule elucidates two important features of the pattern matching machinery of the TWB. First we notice that we used lower case to identify the schemas { a } ; { ~ a }. In the pattern definitions, lowercase always match atoms, while uppercase match both atoms and formulae. In this instance we want to restrict the application of the rule Id only to atoms. Secondly, when the same identifier is used more then once in the definition of a formula schema, the TWB machinery will try to unify it with other occurrences. In this case the rule will be applicable if and only if, the atom a occurs both positively and in the formula ~ a .
RULE And { A & B } ; X ======================= A ; B ; X END
The rule And is a rewriting rule. The body of the rule is composed by a principal formula and an anonymous set. If there is at least one formula in the current tableau node containing a conjunction (eg. a & b), then the rule is applicable. Then the denominator of the rule, breaks down the conjunction into its conjuncts and copies across all the other formulae in the node untouched.
RULE And { A & B } === A ; B END and we will often use this formulation in the remainder of this tutorial. RULE And A & B === A ; B END
ANSWER: In the first case, the rule will choose one single &-formula as principal formula. In the second case all &-formulae will be chosen at once in one rule application. But note that the subformula (d & e) below is not touched because it is not at the top-level in node 1.
#echo "(a & b) & (c & (d & e)) " | ./pc.twb --trace --noneg And ( 0 -> 1 ) (a & b) ; (c & (d & e)) And ( 1 -> 2 ) a ; b ; c ; d & e ; Time:0.0000 Result:Open Total Rules applications:2
RULE Or { A v B } ====================== A | B END
First note, that there is no ancillary X in the numerator or denominator in keeping with the just mentioned note which allows us to assume that all other formulae in the node are left untouched.
The Or rule matches a disjunction and creates two new branches that will be explored by the tableau procedure. The semantics of the Or rule requires both branches to be closed, for the tableau rooted at the current node to be closed. This semantics is enforced by using the single bar "|" as the separator between two branches. In particular, the single bar imposes a condition on backtracking whether to explore the next branch or not. To understand how the TWB works in this instance we need to introduce the notion of visit more in details. By default, the TWB uses a left-to-right depth-first visiting strategy. When the strategy is invoked with the current node, first an applicable rule is selected, then the rule is applied and the strategy is re-invoked on all branches that result from the rule application. On backtrack, that is, when the visit function returns from the visit of a branch, a branching condition is checked to decide whether to explore the next branch. In this particular instance the visit condition will check if the visit of the first branch lead to a closed tableau. If this is the case, the second branch is explored. Otherwise a result of an open branch is immediately returned.
EXERCISE: Consider the variant Or-rule below:
RULE Or-wrong A v B ====================== A | B END
How does it differ from the previous Or-rule, and more importantly, is it semantically sound given our usual interpretation of the classical disjunction?
STRATEGY := tactic ( (Id ! False ! And ! Or)* )
PP := List.map nnf NEG := List.map neg MAIN
The PP directive defines a PreProcessor as indicated by the function to the right of the := sign. If PP is defined then the TWB first uses this preprocessor on all input formulae.
The NEG directive defines a NEGation function as indicated by the function to the right of the := sign. By default, the TWB NEGates all input formulae using this function.
The preprocessor PP is invoked *after* the NEGation function so the directives in this case tell the TWB to NEGate all inputs, and then put the result into nnf by pushing negations down to atomic level.
The MAIN directive just tells the TWB to link the default command line application to the prover. In principle it would be possible to specify different routine, for example to run the prover as a cgi from the web. This is still work in progress.
The TWB (despite the name) is a generic tableau/sequent engine. In this section we give a simple sequent calculus for classical propositional logic. We point out only the differences with the tableau interface. For reference see k_ml_tableau_prover_normal_modal_logic_k
CONNECTIVES [ "~" ; "&" ; "v" ; "->" ; "<->" ; "=>"] GRAMMAR formula := ATOM | Verum | Falsum | formula & formula | formula v formula | formula -> formula | formula <-> formula | ~ formula ;; expr := formula ;; node := set => set ;; END SEQUENT RULE Id Close === { A } => { A } END RULE False Close === { Falsum } => END RULE True Close === => { Verum } END RULE AndL A ; B => === { A & B } => END RULE AndR => A | => B === => { A & B } END RULE OrL A => | B => === { A v B } => END RULE OrR => A ; B === => { A v B } END RULE NegR A => === => { ~ A } END RULE NegL => A === { ~ A } => END RULE ImpL => A | B => === { A -> B } => END RULE ImpR A => B === => { A -> B } END RULE IffL (A -> B) & (B -> A) => === { A <-> B } => END RULE IffR => (A -> B) & (B -> A) === => { A <-> B } END END let exit = function |"Open" -> "Not Derivable" |"Close" -> "Derivable" |s -> assert(false) EXIT := exit(status@1) STRATEGY := tactic ( ( Id ! True ! False ! NegL ! NegR ! AndL ! AndR ! ImpL ! ImpR ! OrL ! OrR ! IffL ! IffR )* ) MAIN
The negation normal form function is written in the TWB as the following Ocaml function:
source Pc let neg = function formula ( a ) -> formula ( ~ a ) let rec nnf = function |formula ( a & b ) -> formula ( {nnf a} & {nnf b} ) |formula ( ~ ( a & b ) ) -> formula ( {nnf formula ( ~ a )} v {nnf formula ( ~ b )} ) |formula ( a v b ) -> formula ({nnf a} v {nnf b}) |formula ( ~ ( a v b ) ) -> formula ( {nnf formula ( ~ a )} & {nnf formula ( ~ b )} ) |formula ( a <-> b ) -> formula ( {nnf formula ( a -> b )} & {nnf formula ( b -> a )} ) |formula ( ~ ( a <-> b ) ) -> formula ( {nnf formula ( ~ (a -> b) )} v {nnf formula ( ~ (b -> a) )} ) |formula ( a -> b ) -> nnf formula ( (~ a) v b ) |formula ( ~ (a -> b) ) -> nnf formula ( a & (~ b) ) |formula ( ~ ~ a ) -> nnf a |formula (Verum) -> formula (Verum) |formula (Falsum) -> formula (Falsum) |formula (~ Verum) -> formula (Falsum) |formula (~ Falsum) -> formula (Verum) |formula ( ~ A ) as f -> f | _ as f -> f
We assume this function to be in a file pclib.ml. The file is then included in the the main logic module by using the directive Open Pclib.
In this section we analyze two variants of a simple tableau calculus for mono-modal logic K. We use this example to explain various parts of the TWB tableau language in detail.
The normal modal logic K (for Kripke) is the simplest normal modal extension of classical logic. In addition to the usual connectives from classical propositional logic, it contains two unary connectives which originally were intended to capture the notions of Necessary and Possibility.
The connectives are usually called "box" and "diamond" nowadays and are often written as [] and <> respectively. The intended semantics of []A is that "A is necessary" and that of <>A is that "A is possible". These connectives are negation duals in that []A can be defined as ~ <> ~ A and <>A can be defined as ~ [] ~ A. Thus we can extend negation normal form to modal logic K simply by pushing negations inwards using these definitions. More precisely, we transform ~ [] A to <> ~ A and transform ~ <> A to [] ~ A (and then transform ~ A recursively).
CONNECTIVES [ "~";"&";"v";"->";"<->";"<>";"[]" ] GRAMMAR formula := ATOM | Verum | Falsum | formula & formula | formula v formula | formula -> formula | formula <-> formula | [] formula | <> formula | ~ formula ;; expr := formula ;; END open Twblib open Klib TABLEAU RULE K { <> A } ; [] X ; Z -------------------- A ; X END RULE Id { a } ; { ~ a } === Close END RULE False Falsum === Close END RULE And { A & B } === A ; B END RULE Or { A v B } === A | B END END STRATEGY := tactic ( (Id ! False ! And ! Or ! K)* ) PP := List.map nnf NEG := List.map neg MAIN We focus on the definition of the K rule. Details regarding the propositional part of the tableau can be seen in pc_ml.
RULE K { <> A } ; [] X ; Z --------------------------------- A ; X END
The K rule body is composed by a principal formula, a possibly empty set of box formulae []X and an anonymous set Z. Note that the K rule is written with a single line "----------" instead of a double line. Intuitively the single lines set an existential backtracking point. In section rule_backtrack we explain in details the three types of backtracking that are allowed in the TWB. For the moment we focus on the semantic of the K rule. The numerator of the rule selects one principal formula, namely <> A. all other occurrences of <>-formulae are matched by the anonymous set Z . Since the set Z is not copied in the denominator (the K rule is not-invertible) once the choice is made, all other diamonds in the set Z will be lost. The single line "---------" set a backtracking point in case the choice of a particular diamonds didn't lead to a closed tableau. That is, imagine we the current node is composed by "<> a & <> b & [] ~ a". Then choosing <> a first will erroneously lead to an open tableau. But choosing <> b first will give a closed tableau. The TWB will backtrack over the choices of <>-formulae to avoid this problem.
echo "<> b & <> a & [] ~ a" | ./k.twb --trace --noneg And ( 0 -> 1 ) ([ ] (~ a)) ; ((<> b) & (<> a)) And ( 1 -> 2 ) (<> a) ; (<> b) ; ([ ] (~ a)) K ( 2 -> 3 ) a ; (~ a) Id ( 3 -> 4 ) Time:0.0000 Result:Close Total Rules applications:4
STRATEGY := tactic ( (Id ! False ! And ! Or ! K)* )This strategy is equivalent to the following strategy: STRATEGY := let sat = tactic ( (Id ! False ! And ! Or) ) in tactic ( ((sat)* ; K )* )
RULE K { <> A } ; [] X ; <> Y ; Z =========================== A ; X || <> Y ; [] X END
The body of the K is composed of a principal formula, a possibly empty set of box formulae []X, a possibly empty set of diamond formulae <>Y and an anonymous set Z. Note that now because of the presence of the schema <>Y, the set Z is diamond-formulae free.
The denominator has two branches.
Note also that we now use the double line as the rule has been determinised and no backtrack is needed to recover from a wrong choice. Moreover the double bar || set an existential branching whose semantic is exactly as outlined before. The second branch is explored if and only if the result of the tableau rooted with the node A ; X is open.
This formulation gives more control over the recursion and allows the user ... HELP ...
In this section we give a tableau calculus for the logic KT.
The logic KT is obtained by adding the axiom []A -> A to the standard Hilbert calculus for K. Semanticall it is characterised by Kripke frames where the reachability relation R is reflexive: that is, every world is reachable from itself.
source K module FormulaSet = TwbSet.Make( struct type t = formula let to_string = formula_printer let copy s = s end ) HISTORIES BOXES : FormulaSet.set := new FormulaSet.set END open Twblib open Klib TABLEAU RULE T { [] A } ========= A ; [] A COND notin(A, BOXES) ACTION [ BOXES := add(A,BOXES) ] END RULE K { <> A } ; [] X ; Z ------- A ; X ACTION [ BOXES := clear(BOXES) ] END RULE Id { a } ; { ~ a } === Close END RULE False Falsum === Close END RULE And { A & B } === A ; B END RULE Or { A v B } === A | B END END STRATEGY := let sat = tactic ( (Id ! False ! And ! Or ! T) ) in tactic ( ((sat)* ; K )* ) PP := List.map nnf NEG := List.map neg MAIN
source K. The effect of this directive is to import the grammar definitions.Since the principal formula []A of the T rule is copied into the denominator, a naive tableau can give rise to a loop, that is an infinite sequence of T-rule applications. To avoid this misbehavior we use a history. We first declare the ocaml object, then we make the history BOXES known to the TWB engine. module FormulaSet = TwbSet.Make( struct type t = formula let to_string = formula_printer let copy s = s end ) HISTORIES BOXES : FormulaSet.set := new FormulaSet.set END See defining_histories_and_variables for a more detailed explanation on how to declare histories and variables.
The tableau calculus for KT is similar to the tableau calculus for K explained in the section k_ml_tableau_prover_normal_modal_logic_k . Here we focus on the rule T and in particular on the use and manipulation of the history.
RULE T { [] A } ============ A ; [] A COND notin(A, BOXES) ACTION [ BOXES := add(A,BOXES) ] END
The body of the rule T simply matches a principal formula [] A and adds A ; [] A to the denominator leaving all other formulae in the node untouched. Obviously, since we copied the formula [] A back in the denominator, the same rule will be again applicable to it, leading to a loop. To stop the loop from happening we put a side-condition on the application of the rule via the COND declaration. The side-condition is true iff the formula A is not in the set BOXES. If the side-condition is true, then the T-rule will be applied. We now need to record that this []A has had the T-rule applied to it so we specify an ACTION to add the formula A to the history BOXES (which is of type a set of formulae). Thus we use the history BOXES to record all the box formulae that we have already encountered and apply the T-rule only to previously unencountered []-formulae.
The action part is introduced by the keyword ACTION. An action is an operation to modify a history or it is an arbitrary function that does not return any value (actually that returns the ocaml type unit). In our example we assigned the result of the ocaml function add() to the history BOXES.
The function add() is specified in the file twblib.ml that contains a number of common functions. In particular it is defined as follows:
(* add : (formula list * Formula.set) -> Formula.set *) let add (l,h) = h#addlist l
See twbset_api for an overview of the methods of the class TwbSet.
Since the logic is reflexive, but not transitive, we must empty the BOXES history after each modal jump. This is done in the action section of the K rule.
RULE K { <> A } ; [] X ; Z ---------------------------------- A ; X ACTION [ BOXES := clear(BOXES) ] END
the function clear is defined as follows: (* Formula.set -> Formula.set *) let clear h = h#empty
We now give an implementation of a tableau calculus for the basic modal logic S4. We use a tableau version of the sequent calculus from Heuerding.
In the following we use two histories, DIAMONDS for the diamond history and BOXES for the box history. Intuitively, the diamond history contains certain diamond formulae found in the branch from the root to the current node. The box history contains all the boxes found in the branch from the root to the current node.
The modal tableau rules shown below are an adaptation of Heuerding's sequent rules. source K module FormulaSet = TwbSet.Make( struct type t = formula let to_string = formula_printer let copy s = s end ) HISTORIES DIAMONDS : FormulaSet.set := new FormulaSet.set; BOXES : FormulaSet.set := new FormulaSet.set END open Twblib open Klib TABLEAU RULE S4 { <> A } ; Z --- A ; BOXES COND notin(<> A, DIAMONDS) ACTION [ DIAMONDS := add(<> A,DIAMONDS) ] END RULE T { [] A } === A COND notin(A, BOXES) ACTION [ BOXES := add(A,BOXES); DIAMONDS := emptyset(DIAMONDS)] END RULE Id { a } ; { ~ a } === Close END RULE False Falsum === Close END RULE And { A & B } === A ; B END RULE Or { A v B } === A | B END END STRATEGY := let sat = tactic ( (False ! Id ! And ! T ! Or) ) in tactic ( ( (sat)* ; S4 )* ) PP := List.map nnf NEG := List.map neg MAIN
In particular the (T)-rule is applied to a principal formula [] P only if its sub-formula P is not in the history BOXES. If notin(P,BOXES) , the denominator is created from the current rule by deleting [] P and adding P. The formula P is added to the history BOXES and the diamond history DIAMONDS is emptied.
RULE T { [] A } ======== A COND notin(A, BOXES) ACTION [ BOXES := add(A,BOXES); DIAMONDS := emptyset(DIAMONDS)] END
Since the Kripke models for the logic S4 are transitive, box formulae always accumulate. In the calculus, the (T)-rule is applied only if the immediate sub-formulae P of the box formula [] P under consideration is "new" (not present in the box history) in the branch, thus exploiting transitivity. Intuitively, if a box formula is new in a branch, we force the procedure "to recompute", by forgetting (empting DIAMONDS) any information about the diamond formulae found so far.
RULE S4 { <> A } ; Z ----------------- A ; BOXES COND notin(<> A, DIAMONDS) ACTION [ DIAMONDS := add(<> A,DIAMONDS) ] END
Similarly, the S4 rule is applied only if its diamond formula <> P is not present in the diamond history DIAMONDS. If notin(<>P,DIAMONDS), then the formula P and the content of the box history DIAMONDS is added to the denominator. The context Z is discarded and the formula <> P is the diamond history DIAMONDS. The box history BOXES is unchanged.
let add (l,h) = h#addlist l let notin (l,h) = not(h#mem (List.hd l)) let emptyset h = h#empty