"Set Theory for Computing" provides a comprehensive account of set-oriented symbolic manipulation methods suitable for automated reasoning. Its main objective is twofold: 1) to provide a flexible formalization for a variety of set languages, and 2) to clarify the semantics of set constructs firmly established in modern specification languages and in the programming practice. Topics include: semantic unification, decision algorithms, modal logics, declarative programming, tableau-based proof techniques, and theory-based theorem proving. The style of presentation is self-contained, rigorous and...

An up-to-date and comprehensive account of set-oriented symbolic manipulation and automated reasoning methods. This book is of interest to graduates and researchers in theoretical computer science and computational logic and automated reasoning.

This treatise presents an integrated perspective on the interplay of set theory and graph theory, providing an extensive selection of examples that highlight how methods from one theory can be used to better solve problems originated in the other.

This book presents a set of historical recollections on the work of Martin Davis and his role in advancing our understanding of the connections between logic, computing, and unsolvability.