Tutorial: The Tableau Work Bench: Theory and Practice

===Level: === You should know the basics of tableau/sequent calculi as explained in the Handbook of Tableau Methods (for example). Only rudimentary programming knowledge is required but basic functional programming knowledge would be ideal. 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. ===Abstract:=== Tableau/sequent calculi are now a standard method for automating deduction in non-classical logics. The currently available avenue for rapid prototyping of your favourite tableau/sequent calculus is to modify LeanTAP since general logical frameworks like Coq, ELF, Isabelle and NuPrl take months to master and existing provers like the Logics Work Bench provide only a fixed number of logics. The TWB is a generic tableau framework for building tableau/sequent-based theorem provers for (non-classical) propositional logics. 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.

Basic Notions

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.

Architecture

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: *Sequence: Since OCaml is by design an eager language, we avoid wasteful computations by using a generic lazy list (library) to construct the proof tree; * Tree: Defines the proof tree data type; * Node: Defines a node as a generic container which encapsulates arbitrary data structures (like sets, multi-sets, sequences, etc.); * Rule: Implements the interface to define logical rules in the TWB. A rule can be seen as a re-writing function that is applied if a pre-condition is met. Defines the interface for specifying rules; * Visit: The Visit module implements the core algorithm to generate and visit the proof tree given the current node and the current state of the strategy.

Core Algorithm

[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''). * Rule condition: this function is used by the strategy procedure and checks if a rule is applicable to the current node and if the side conditions of the rule are satisfied. The result of this function is a partition of the current node according to the patterns specified in the numerator of the selected rule. * Rule action: this function accepts a rule that has been selected and applies it to the current node to expand the proof tree. The result of this function is a list of nodes, each identifying a new branch in the proof tree. *Branch condition: this function is executed after visiting the i^th sub-tree rooted at the current node to determine if the sub-tree created so far (including all the already visited branches) satisfies a logic-specific condition. If so, the visit explores the next branch (if any), otherwise, the visit is interrupted and the procedure backtracks. * Rule backtrack: these functions are executed after all branches (or a number of them according to the branch condition) are visited to synthesise their results into one result for the current node and pass it up to its parent.

Removing Non-Determinism

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: *Node-choice: the algorithm chooses which leaf becomes the current node; *Rule-choice: the algorithm chooses which rule to apply to the current node; *Instance-choice: the algorithm chooses which formula to make the principal formula for the chosen rule and the chosen current node. That is, it determines the order in which to explore the different instantiations (partitions) of the current node created by the chosen rule. ==Node-choice== The first source of non-determinism is which (leaf) node to select as the current node and is usually handled by a visit algorithm that selects this node out of possibly many in the current tree. For exposition, we use a depth first visit function that deterministically selects the left most node, but our algorithm allows any visit strategy to be used to explore the search space (ie. breadth-first). ==Rule-choice== The second source of non-determinism in tableau methods arises from the lack of guidance when applying logical rules. If a node contains many different formulae, then many rules may be applicable to that node. How to choose? 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. ==Instance-choice== The third form of non-determinism is the aforementioned choice of one rule instance (partition) of the current node from potentially many rule instances (partitions) of the current node. Then, this nondeterminism can be resolved by using optimisation techniques based on logic-specific considerations used to reduce the size of the search space. For example, if the chosen rule is an Or-rule, heuristics such as MOMS (Maximum number of Occurrences in disjunctions of Minimum Size) or iMOMS (inverted MOMS) order the disjunctions (formulae) in the node to always choose the less/more constrained disjunct, which, in principle, should lead to an earlier clash.

Backtracking

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.

Defining Histories and Variables

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: * TwbSet.Make ( ElementTYPE ) : defines a set of elements of type ElementTYPE * TwbMSet.Make ( ElementTYPE ) : defines a multi set of elements of type ElementTYPE * TwbList.Make ( ElementTYPE ) : defines a list of elements of type ElementTYPE 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

TwbSet API

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 * method add : 'basetype -> 'typesettype : add en element of type 'basetype to the object and return the modified object. Example: (* add : (formula list * Formula.set) -> Formula.set *) let add (l,h) = h#addlist l * method add_filter : ('basetype -> 'basetype -> bool ) -> 'basetype -> 'typesettype * method addlist : 'basetype list -> 'typesettype : add a list of elements * method del : 'basetype -> 'typesettype : remove one element * method mem : 'basetype -> bool : check if an element is present * method elements : 'basetype list : return the list of element in the object * method hd : 'basetype : return an element of the object. If the data type is implemented as a list, then it returns the first element of the list, otherwise it returns an unspecified element of the collection. * method is_empty : bool : check if the object is empty * method filter : ('basetype -> bool) -> 'typesettype * method length : int : returns the cardinality of the object * method cardinal : int : same as ''length'' * method intersect : 'typesettype -> 'typesettype * method union: 'typesettype -> 'typesettype * method subset: 'typesettype -> bool * method is_equal : 'typesettype -> bool * method copy : 'typesettype : return a deep copy of the object * method empty : 'typesettype : return an empty instance of the object * method to_string : string : return a string containing the human readable representation of the object

Defining the Strategy

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

Introduction and Examples

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.

Compilation and Running of the TWB

===Compilation=== 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. ===Running .twb files=== 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.'''' ====Command Line Options==== 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 : * ''--noneg'' is the runtime option to switch off the negation of the input formula. This is useful when 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. * ''--nopp'' disables the preprocessing function. In our example, the negation normal form function nnf is the pre-processing function PP. * ''--trace'' enables a rule by rule trace of the proof. By default the twb outputs only the outcome of the proof. By tracing the proof it is possible to do a step by step analysis of the proof. Useful for debugging. * ''--verbose'' displays additional information $./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

pc.ml: A Tableau Prover for Classical Propositional Logic

===Connectives=== 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. ====Restrictions==== * The backslash symbol "\" cannot be used. * The symbol vertical bar "|" cannot be used. * Double semicolon ";;" cannot be used. * The string "ATOM" cannot be used. * The symbols "(", ")", "{" , "}" cannot be used. ===Grammar=== 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''. * node: this production defines the shape of a tableau/sequent node. By default, a tableau node is composed of a set of formulae. * expr: this production defines the outer most expressions used in the definition of tableau rules. Generally an expression is just a formula. In more complicated tableau rules, an expression can be a formula decorated with a label or with another arbitrary data structure. * formula : this production defines the shape of the formula definition to be used in the tableau rules. ====Conventions==== * Lower case identifier in a production are interpreted as a grammar identifier for a production. * Upper case identifiers are interpreted as constants (eg. Verum and Falsum). * The keyword '''ATOM''' identifies an atom in the grammar. ====Restrictions==== The grammar accepted by the TWB is a loose LL(1) grammar. Conflicts are not handled automatically and the definition of ambiguous grammars can lead to unspecified results. ====NOTA BENE==== At the moment of writing the grammar machinery still has some minor bugs that we are seeking to address in future releases. ===OCaml Code === 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 Definition=== 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: *Numerator: The numerator is a list of formula schemas separated by semicolons and specifies a partition of the current node in the proof tree. Formulae schemas are parsed according to the connectives declared in the connectives section with principal formulae enclosed in braces { }. A pattern is ''restricted'' if it is specified by a formula schema containing connectives like A -> B and Box A. A pattern is {\em unrestricted} if it is specified by just a meta-variable like X. There may be many ways of partitioning a node to match the pattern specified by the numerator leading to implicit choice-points. * Separator: A rule commits to the first numerator pattern choice if the separator between the numerator and denominators is a sequence of at least two "='' symbols. A rule backtracks over the different pattern choice-points if the separator is a sequence of at least two ``-'' symbols and the current partition choice does not close. Intuitively, a rule that commits is declared to be invertible and a rule that does not commit is declared to be non-invertible. However, the TWB does not check that the rule is really invertible. It assumes that the user has proved an inversion lemma independently. * Denominator: In general, a rule can have a list of denominators related by a branching operator. Each denominator is a list of formula schemas and specifies how to construct the root nodes of the branches that extend the tableau using the patterns assigned to the meta-variables in the numerator. The (universal) branch separator | is an instruction to close the current node if ''every'' denominator closes. The (existential) branch separator || is an instruction to close the current node if ''some'' denominator closes. These are actually instances of conditional branching which are instructions to close the current node if the denominators meet a specified condition. * Cond: A rule is applicable if the side-conditions are satisfied as specified using the COND construct. If all the side conditions are true, then the tentative partition is accepted. Otherwise the partition is not considered and the pattern matching algorithm proceeds until a successful partition is found. * Action: If the rule is applicable then the ACTION construct specifies actions on the current histories or variables to compute the histories of the children. * Branch: Conversely, branch conditions, specified by the keyword BRANCH, are executed on backtracking to check whether to explore the next branch (if there is one) or to backtrack further. It is possible to specify a list of branch conditions, one for every branch and each set of branch conditions will have access to all variables returned by any branch already explored. An attempt to access a variable related to a branch yet to be visit will generate a run-time error. * Backtrack: Specifies how to synthesize the result for the current node from the results of the children. ====We now analyze each rule definition:==== 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. ====Note==== Even if it is always possible to specify the anonymous set in the rule schemas, this is not recommended. The default of the TWB is to leave untouched all formulae that are not explicitly manipulated by a rule application. The previous rule could have also been written as RULE And { A & B } === A ; B END and we will often use this formulation in the remainder of this tutorial. ------------- EXERCISE: how does the following rule differ operationally from the And rule above? 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=== STRATEGY := tactic ( (Id ! False ! And ! Or)* ) ===Operators=== 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.

pcseq.ml : a sequent calculus for classical proposition logic

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

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.

k.ml: A Tableau Prover for Normal Modal Logic K

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. ==Modal Logic K== 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). ==A simple tableau for K== 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. ====Example==== 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=== The strategy specifies the order in which rules are applied during proof search. In our example, for completeness, we need to apply all classical rule first and then the K rule. The bang '''!''' operator applies the first rule that is applicable. The star '''*''' iterates until one rule is applicable. Since the K rule is the last rule, this means that all the other rules are not applicable. 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 )* )

k.ml: explicit branching

===Using || for K Rule=== In [[k_ml_tableau_prover_normal_modal_logic_k]] we specified the '''K''' rule using s single line and hence implicit backtracking. Now we specify the same rule by making the backtracking explicit. The '''K''' rule can also be written as follows: 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. * '''A ; X''' encodes the modal jump * '''<> Y ; [] X''' encodes a recursion step to consider all other diamonds if the first branch didn't lead to a closed tableau. 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 ...

kt.ml: Modal Logic KT Using Histories

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 ===Step by step explanation=== The module for the logic KT does not begin with a CONNECTIVES and GRAMMAR specification, but we recycle the definition in the file ''k.ml'' using the directive 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

s4.ml: Modal Logic S4 Using Histories

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. ====Functions==== In particular, we use three functions to handle histories: let add (l,h) = h#addlist l let notin (l,h) = not(h#mem (List.hd l)) let emptyset h = h#empty * '''notin(formula list, history)''': accepts a list of formulae and a history, and returns a boolean indicating if the list of formulae is in the history. * '''add(formula list, history)''': accepts a list of formulae and a history object and returns the history object with the formula list added to it. * '''emptyset(history)''': returns an empty history object. ====Note==== The rules described in this section assume a decision procedure that first applies all classical rules and the (T)-rule until they are no longer applicable; and then which applies the modal rule S4. Therefore, in the (S4)-rule, the set '''Z''' will consist of all diamond formulae in the node except '''<> P''' and literals only. In particular, since the (T)-rule removes all box formulae from the node and stores their immediate sub-formulae in the box history '''BOXES''', then the set '''Z''' will be box-free.