Dual tableaux. Foundations, methodology, case studies (Q710340)

This book presents a complete dual tableaux theory which includes the description of foundations and methodology of this approach to logical systems through a widespread variety of examples such as classical first-order logic (with or without identity), non-classical logics (superintuitionistic, modal, temporal, relevant and multiple-valued), logics of programs, fuzzy logics, logics of rough sets, theories of spatial reasoning, theories of order of magnitude reasoning, and formal concept analysis. The concept of dual tableaux was introduced by \textit{H. Rasiowa} and \textit{R. Sikorski} [Fundam. Math. 48, 57--69 (1960; Zbl 0099.00603)] as a realization of the Beth idea of the analytic tableau system [see \textit{E. W. Beth}, The foundations of mathematics. A study in the philosophy of science. Amsterdam: North-Holland Publishing Company (1959; Zbl 0085.24104)]. The dual tableaux method is based on the following two methodological principles: (a) for a given theory, a truth-preserving translation of the language of the theory into an appropriate language of (most often binary) relations is defined, and (b) for this relational language, providing a deduction system for the original theory, a dual tableau is constructed. These principles enable us to represent, within a uniform formalism, the three basic components of a formal system: its syntax, including its deduction apparatus, and the corresponding semantics. The relational approach makes it possible to build dual tableaux in a systematic modular way and performs not only verification of validity but can often be used for proving entailment, model checking and satisfaction. The material of the book is presented in 7 parts, divided into 25 chapters. Part I (Foundations: Dual tableau for classical first-order logic; Dual tableaux for logics of classical algebras of binary relations; Theories of point relations and relational model checking) deals with the two systems providing a foundation for all the dual tableau systems presented in the book. Part II (Reasoning in logics of non-classical algebras of relations: Dual tableaux for Peirce algebras; Dual tableaux for fork algebras; Dual tableaux for relational databases) is devoted to some non-classical theories of relations, including a theory of typed relations making it possible to represent relations as they are understood in relational databases. Part III (Relational reasoning in traditional non-classical logics: Dual tableaux for classical modal logics; Dual tableaux for some logics based on intuitionism; Dual tableaux for relevant logics; Dual tableaux for many-valued logics) deals with a relational formalization of modal logics, some logics in the neighborhood of Heyting's logic (Johansson's, Scott's and the logic of weak excluded middle), relevant and many-valued logics. In Part IV (Relational reasoning in logics of information and data analysis: Dual tableaux for information logics of plain frames; Dual tableaux for information logics of relative frames; Dual tableau for formal concept analysis; Dual tableau for a fuzzy logic; Dual tableaux for logics of order of magnitude reasoning) the major theories of reasoning with incomplete information are considered. Part V (Relational reasoning about time, space, and action: Dual tableaux for temporal logics; Dual tableaux for interval temporal logics; Dual tableaux for spatial reasoning; Dual tableaux for logics of programs) is concerned with temporal and spatial reasoning and logics of programs, including a system for the region connection calculus, as well as various versions of propositional dynamic logic. Part VI (Beyond relational theories: Dual tableaux for threshold logics; Signed dual tableau for Gödel-Dummett logic; Dual tableaux for first-order Post logics; Dual tableau for propositional logic with identity; Dual tableaux for logics of conditional decisions) deals with some theories for which dual tableau systems are constructed directly within the theory, without translation into any relational theory. In the single chapter of the concluding Part VII (Conclusion: Methodological principles of dual tableaux), the authors accomplish a synthesis of what was considered in the preceding chapters, collect observations on how the dual tableaux rules should be designated once the constraints on the models of the theories or definitions of some specific constants are given, and, finally, discuss some useful strategies for the construction of dual tableaux proofs. Providing a reference for researchers and students, this book presents the fundamental concepts of dual tableaux and a wide scope of applications. These include logic methods used in mathematics and philosophy as well as applied theories of computational logic.