Completed in 1983, this work culminates nearly half a century of the late Alfred Tarski's foundational studies in logic, mathematics, and the philosophy of science. Written in collaboration with Steven Givant, the book appeals to a very broad audience, and requires only a familiarity with first-order logic. It is of great interest to logicians and mathematicians interested in the foundations of mathematics, but also to philosophers interested in logic, semantics, algebraic logic, or the methodology of the deductive sciences, and to (...) computer scientists interested in developing very simple computer languages rich enough for mathematical and scientific applications. The authors show that set theory and number theory can be developed within the framework of a new, different, and simple equational formalism, closely related to the formalism of the theory of relation algebras. There are no variables, quantifiers, or sentential connectives. Predicates are constructed from two atomic binary predicates (which denote the relations of identity and set-theoretic membership) by repeated applications of four operators that are analogues of the well-known operations of relative product, conversion, Boolean addition, and complementation. All mathematical statements are expressed as equations between predicates. There are ten logical axiom schemata and just one rule of inference: the one of replacing equals by equals, familiar from high school algebra. Though such a simple formalism may appear limited in its powers of expression and proof, this book proves quite the opposite. The authors show that it provides a framework for the formalization of practically all known systems of set theory, and hence for the development of all classical mathematics. The book contains numerous applications of the main results to diverse areas of foundational research: propositional logic; semantics; first-order logics with finitely many variables; definability and axiomatizability questions in set theory, Peano arithmetic, and real number theory; representation and decision problems in the theory of relation algebras; and decision problems in equational logic. (shrink)

We present two proof systems for first-order logic with identity and without function symbols. The first one is an extension of the Rasiowa-Sikorski system with the rules for identity. This system is a validity checker. The rules of this system preserve and reflect validity of disjunctions of their premises and conclusions. The other is a Tableau system, which is an unsatisfiability checker. Its rules preserve and reflect unsatisfiability of conjunctions of their premises and conclusions. We show that the two systems (...) are dual to each other. The duality is expressed in a formal way which enables us to define a transformation of proofs in one of the systems into the proofs of the other. (shrink)

The Description Logic Handbook covers all aspects of the research in the field of knowledge representation. Written by some of the most prominent researchers in the field, and covering the basic technical material and implementational aspects, it is both a unique reference and a self-study guide.

The book presents logical foundations of dual tableaux together with a number of their applications both to logics traditionally dealt with in mathematics and philosophy (such as modal, intuitionistic, relevant, and many-valued logics) and to various applied theories of computational logic (such as temporal reasoning, spatial reasoning, fuzzy-set-based reasoning, rough-set-based reasoning, order-of magnitude reasoning, reasoning about programs, threshold logics, logics of conditional decisions). The distinguishing feature of most of these applications is that the corresponding dual tableaux are built in a (...) relational language which provides useful means of presentation of the theories. In this way modularity of dual tableaux is ensured. We do not need to develop and implement each dual tableau from scratch, we should only extend the relational core common to many theories with the rules specific for a particular theory. (shrink)

The purpose of the present paper is to show that modal propositional logics can be interpreted in a logic based on relational calculus. We consider languages with necessity operators [R], where R is an accessibility relation expression representing an element of the algebra of binary relations with operations −,∪,∩, −1 , ◦. The relational logic is based on relational calculus enriched by operations of weakest prespecification and weakest postspecification introduced in Hoare and He Jifeng and investigated in He Jifeng et (...) al . The logic is an extension of the system introduced in Or lowska and investigated in Buszkowski and Or lowska. (shrink)