Overseas Visit in Automated Model Building

这些项目要求资助首席研究员到澳大利亚信息和通信技术卓越研究中心NICTA（堪培拉）进行一次短期海外访问，以便与Peter Baumgartner教授和Rajeev戈尔博士就自动化模型构建问题进行合作。Baumgartner教授是自动推理领域的领先专家，拥有与模型构建和一阶定理证明相关的特殊专业知识。他在实例化方法、一阶Davis-Putnam、模型生成以及定理证明器的开发和实现方面拥有丰富的专业知识。戈尔博士是一位著名的证明理论和非经典逻辑专家，包括tableaux方法、规则语法模态逻辑和描述逻辑。该项目有两个主要目标：（i）研究自下而上模型生成方法的范式，并致力于开发更强大、更有效和更通用的模型生成方法。(ii)利用已开发的技术设计和实现描述逻辑和模态逻辑的新模型生成和自动推理方法。模型构建对于测试，验证和验证目的非常重要，例如，软件测试，多代理系统测试，本体验证，本体推理机验证。它们可以用于故障分析、系统验证，也可以用于数据模型的验证。

The projects requests funding for a short overseas visit of the PI to NICTA (Canberra), Australia's ICT Research Centre of Excellence, in order to work together with Prof Peter Baumgartner and Dr Rajeev Gore on the topic of automated model building. Prof Baumgartner is a leading expert in the area of automated reasoning with special expertise relating to model building and first-order theorem proving. He has extensive expertise in instantiation methods, first-order Davis-Putnam, model generation and the development and implementation of theorem provers. Dr Gore is a well-known expert in proof theory and non-classical logic, including tableaux methods, regular grammar modal logics and description logics.The project has two main objectives: (i) Investigating the paradigm of bottom-up model generation methods and work on the development of stronger, more efficient and more general model generation methods. (ii) Exploiting the developed techniques for devising and implementing novel model generation and automated reasoning methodologies for description logics and modal-type logics.Model building is hugely important for testing, validation and verification purposes, for instance, software testing, testing of multi-agent systems, validation of ontologies, verification of ontology reasoners. They can be used for fault analysis, verification of systems, and they can be used for validation of data models.