The “tableau” algorithm

• The main steps of the algorithm are (for V ⊧L W ):

• • W is simplified (brought to “normal form”, much like a normal form in predicate logic)
  • a new vocabulary U is defined, combining V and the negation of W such that V ⊧L W is equivalent with U not being consistent (a form of “reductio ad absurdum”)
  • the algorithm tries to construct an interpretation for U , taking into account all possibilities. If:
  • • it succeeds, then U is consistent, i.e., V ⊧L W does not hold
    • if it fails then U is not consistent, ie, V ⊧L W holds

• The complexity of the algorithm depends on the expressiveness of the language (mainly in covering all possibilities when constructing an interpretation)