Practical Automated Deduction

这个项目将开发，实施和验证改进的方法，用于在一阶逻辑的可判定片段中自动推理，还将推理纳入特殊理论，如算术。它将大大扩展以前的工作模型演化演算和动态语义解析，并引入新的技术，结合这些推理方法的联合收割机。这项工作有直接的应用推理业务规则和工业优化问题，它将激励和测试我们的系统通过案例研究，从这两个领域。

This project will develop, implement and validate improved methods for automated deduction in decidable fragments of first order logic, also incorporating reasoning in special theories such as arithmetic. It will significantly extend previous work on the model evolution calculus and dynamic semantic resolution, and introduce new techniques that combine these reasoning methods. This work has direct application to reasoning about business rules and about industrial optimisation problems, and it will motivate and test our systems by means of case studies from both of these areas.