Logic for Computer Scientists/Modal Logic/Modal Logic Tableaux
Modal Logic Tableaux
editIn classical propositional logics we introduced a tableau calculus (Definition) for a logic as a finitely branching tree whose nodes are formulas from . Given a set of formulae from , a tableau for was constructed by a (possibly infinite) sequence of applications of a tableau rule schema:
where the premise as well as the denominators are sets of formulae; is the name of the rule. We introduce -tableau with the help of the following rules:
A tableau for a set of formulae is a finite tree with root whose nodes carry finite formulae sets. The rules for extending a tableau are given by:
- choose a leaf node with label , where is not an end node, and choose a rule , which is applicable to ;
- if has denominators then create successor nodes for , with successor carrying an appropriate instance of denominator ;
- if a successor carries a set and has already appeared on the branch from the root to then is an end node.
A branch is called closed if its end node is carrying , otherwise it is open.
As in the classical case, a formulae is a theorem in modal logic ,
iff there is a closed -tableau for the set .
As an example take the formula : its negation is certainly unsatisfiable, because the formula is an instance of our previously given -axiom.
Some remarks are in order:
- The - rule, called the thinning rule, is necessary in order to construct the premisses for the application of the -rule.
- Both can be combined by a new rule
- In order to get tableau calculi for the other mentioned calculi, like or one has to introduce additional rules:
which obviously reflects reflexivity of the reachability relation, or
reflecting transitivity.