This completely self-contained study, widely considered the best book in the field, is intended to serve both as an introduction to quantification theory and as ...

Inductive theorem proving in the form of descente infinie was known to the ancient Greeks and is the standard induction method of a working mathematician since it was reinvented in the middle of the 17th century. We present an integration of descente infinie into state-of-the-art free-variable sequent and tableau calculi. It is well-suited for an efficient interplay of human interaction and automation and combines raising, explicit representation of variable dependency, the liberalized δ-rule, preservation of solutions, and unrestricted applicability of lemmas (...) and induction hypotheses. The semantical requirements are satisfied for a variety of two-valued logics, such as clausal logic, classical first-order logic, and higher-order modal logic. (shrink)