13 - Tableaux-Based Decision Methods

Summary

The underlying idea of the method of semantic tableaux for testing satisfiability of logical formulae is to organise a systematic search for a satisfyingmodel of the input formula, or set of formulae. Both the entire procedure and the search tree itself are usually called ‘tableau’. The tableau search follows the logical structure of the formulae to be satisfied and consists of repeated application of specific formula decomposition rules associated with the logical connectives in the given logical language. If the search for a satisfying model terminates without success, the tableau is pronounced ‘closed’ and the input set of formulae is declared unsatisfiable. If the tableau method is sound, closure of the tableau search must imply that the input set of formulae is indeed unsatisfiable. If the search succeeds, or never terminates, the tableau is pronounced ‘open’. If the input is not satisfiable, a complete tableau procedure is supposed to terminate and establish that the input is not satisfiable, indeed.

Traditionally tableaux are regarded as logical deductive systems, built in a formal, declarative, rule-based manner. Tableaux for classical logic use only local decomposition rules, while tableaux for modal and temporal logics also involve successor rules and in the traditional versions both types of rules are treated on a par and the control mechanisms are built in as provisos for the application of these rules. While soundness and completeness are sine qua non, termination is not a common requirement. Indeed, in case of logics with undecidable but recursively axiomatisable validity, such as first-order logic, a sound and complete tableau cannot be always terminating, so it can only be used as a deductive system, but not as a decision procedure. In this book we use tableaux as decision procedures, hence in our context termination is a requirement that is as essential as soundness and completeness. Moreover, if a tableau-based search terminates successfully (as open tableau) it usually provides sufficient information to build a model satisfying the input. Thus, a sound, complete and always terminating tableau for a given logic provides not only a decision procedure for testing satisfiability (respectively, validity) in it, but also a constructive method for model building, whenever a model for the input set of formulae exists.