Automated Reasoning

Automated reasoning and knowledge representation are intertwined, as reasoning engines need to take into account representation formalisms and vice versa. The chapter entitled "Automated Reasoning" surveys both. It covers classical and non-classical logics, illustrating relevant trade-offs between expressivity and decidability. It summarizes basic principles and results in theorem proving, model building, decision procedures, model checking, logic programming, with applications ranging from verification and reasoning about action to multi-agent systems and web-based reasoning.