Practical Automated Deduction

We develop, implement and validate improved methods for automated deduction in decidable fragments offirst order logic, also incorporating reasoning in special theories such as arithmetic. We significantly extendour previous work on the model evolution calculus and dynamic semantic resolution, and introduce newtechniques that combine these reasoning methods. This work has direct application to reasoning aboutbusiness rules and about industrial optimisation problems, and we motivate and test our systems by meansof case studies from both of these areas.