Automated Deduction in Nonclassical Logics: Efficient Matrix Proof Methods for Modal and Intuitionistic Logics

This book develops and demonstrates efficient matrix proof methods for automated deduction within an important and comprehensive class of first order and intuitionistic logics. Traditional techniques for the design of efficient proof systems are abstracted from their original setting which allows their application to a wider class of mathematical logic. The logics discussed are used throughout computer science and artificial intelligence.