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.